Skip to content

Commit f052fe2

Browse files
matheusaaguiarmatheusaaguiar
committed
Update cmdline tests
1 parent 011eb3a commit f052fe2

File tree

47 files changed

+587
-18
lines changed
  • test/cmdlineTests
    • model_checker_targets_all_all_engines
    • model_checker_targets_all_bmc
    • model_checker_targets_all_chc
    • model_checker_targets_assert_bmc
    • model_checker_targets_assert_chc
    • model_checker_targets_balance_bmc
    • model_checker_targets_balance_chc
    • model_checker_targets_constant_condition_bmc
    • model_checker_targets_default_all_engines
    • model_checker_targets_default_bmc
    • model_checker_targets_default_chc
    • model_checker_targets_div_by_zero_bmc
    • model_checker_targets_div_by_zero_chc
    • model_checker_targets_out_of_bounds_chc
    • model_checker_targets_overflow_bmc
    • model_checker_targets_overflow_chc
    • model_checker_targets_pop_empty_chc
    • model_checker_targets_underflow_bmc
    • model_checker_targets_underflow_chc
    • model_checker_targets_underflow_overflow_assert_bmc
    • model_checker_targets_underflow_overflow_assert_chc
    • model_checker_targets_underflow_overflow_bmc
    • model_checker_targets_underflow_overflow_chc
    • standard_model_checker_targets_assert_bmc
    • standard_model_checker_targets_assert_chc
    • standard_model_checker_targets_balance_bmc
    • standard_model_checker_targets_balance_chc
    • standard_model_checker_targets_constantCondition_bmc
    • standard_model_checker_targets_constantCondition_chc
    • standard_model_checker_targets_default_all_engines
    • standard_model_checker_targets_default_bmc
    • standard_model_checker_targets_default_chc
    • standard_model_checker_targets_div_by_zero_bmc
    • standard_model_checker_targets_div_by_zero_chc
    • standard_model_checker_targets_out_of_bounds_bmc
    • standard_model_checker_targets_out_of_bounds_chc
    • standard_model_checker_targets_overflow_bmc
    • standard_model_checker_targets_overflow_chc
    • standard_model_checker_targets_pop_empty_bmc
    • standard_model_checker_targets_pop_empty_chc
    • standard_model_checker_targets_underflow_bmc
    • standard_model_checker_targets_underflow_chc
    • standard_model_checker_targets_underflow_overflow_assert_bmc
    • standard_model_checker_targets_underflow_overflow_assert_chc
    • standard_model_checker_targets_underflow_overflow_bmc
    • standard_model_checker_targets_underflow_overflow_chc
    • viair_abicoder_v1

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

47 files changed

+587
-18
lines changed

‎test/cmdlineTests/model_checker_targets_all_all_engines/err‎

Lines changed: 6 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,9 @@
1+
Warning: transfer will be deprecated in the next breaking version
2+
--> input.sol:10:3:
3+
|
4+
10 | a.transfer(x);
5+
| ^^^^^^^^^^
6+
17
Warning: CHC: Underflow (resulting value less than 0) happens here.
28
Counterexample:
39
arr = []
@@ -74,15 +80,6 @@ test.f(0x0, 1)
7480
| ^^^^^^^^^
7581

7682
Warning: CHC: Out of bounds access happens here.
77-
Counterexample:
78-
arr = []
79-
a = 0x0
80-
x = 0
81-
82-
Transaction trace:
83-
test.constructor()
84-
State: arr = []
85-
test.f(0x0, 1)
8683
--> input.sol:13:3:
8784
|
8885
13 | arr[x];

‎test/cmdlineTests/model_checker_targets_all_bmc/err‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,9 @@
1+
Warning: transfer will be deprecated in the next breaking version
2+
--> input.sol:10:3:
3+
|
4+
10 | a.transfer(x);
5+
| ^^^^^^^^^^
6+
17
Warning: BMC: Condition is always true.
28
--> input.sol:6:11:
39
|

‎test/cmdlineTests/model_checker_targets_all_chc/err‎

Lines changed: 6 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,9 @@
1+
Warning: transfer will be deprecated in the next breaking version
2+
--> input.sol:10:3:
3+
|
4+
10 | a.transfer(x);
5+
| ^^^^^^^^^^
6+
17
Warning: CHC: Underflow (resulting value less than 0) happens here.
28
Counterexample:
39
arr = []
@@ -74,15 +80,6 @@ test.f(0x0, 1)
7480
| ^^^^^^^^^
7581

7682
Warning: CHC: Out of bounds access happens here.
77-
Counterexample:
78-
arr = []
79-
a = 0x0
80-
x = 0
81-
82-
Transaction trace:
83-
test.constructor()
84-
State: arr = []
85-
test.f(0x0, 1)
8683
--> input.sol:13:3:
8784
|
8885
13 | arr[x];

‎test/cmdlineTests/model_checker_targets_assert_bmc/err‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,9 @@
1+
Warning: transfer will be deprecated in the next breaking version
2+
--> input.sol:10:3:
3+
|
4+
10 | a.transfer(x);
5+
| ^^^^^^^^^^
6+
17
Warning: BMC: Assertion violation happens here.
28
--> input.sol:11:3:
39
|

‎test/cmdlineTests/model_checker_targets_assert_chc/err‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,9 @@
1+
Warning: transfer will be deprecated in the next breaking version
2+
--> input.sol:10:3:
3+
|
4+
10 | a.transfer(x);
5+
| ^^^^^^^^^^
6+
17
Warning: CHC: Assertion violation happens here.
28
Counterexample:
39
arr = []

‎test/cmdlineTests/model_checker_targets_balance_bmc/err‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,9 @@
1+
Warning: transfer will be deprecated in the next breaking version
2+
--> input.sol:10:3:
3+
|
4+
10 | a.transfer(x);
5+
| ^^^^^^^^^^
6+
17
Warning: BMC: Insufficient funds happens here.
28
--> input.sol:10:3:
39
|

‎test/cmdlineTests/model_checker_targets_balance_chc/err‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1 +1,7 @@
1+
Warning: transfer will be deprecated in the next breaking version
2+
--> input.sol:11:3:
3+
|
4+
11 | a.transfer(x);
5+
| ^^^^^^^^^^
6+
17
Info: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

‎test/cmdlineTests/model_checker_targets_constant_condition_bmc/err‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,9 @@
1+
Warning: transfer will be deprecated in the next breaking version
2+
--> input.sol:10:3:
3+
|
4+
10 | a.transfer(x);
5+
| ^^^^^^^^^^
6+
17
Warning: BMC: Condition is always true.
28
--> input.sol:6:11:
39
|

‎test/cmdlineTests/model_checker_targets_default_all_engines/err‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,9 @@
1+
Warning: transfer will be deprecated in the next breaking version
2+
--> input.sol:10:3:
3+
|
4+
10 | a.transfer(x);
5+
| ^^^^^^^^^^
6+
17
Warning: CHC: Division by zero happens here.
28
Counterexample:
39
arr = []

‎test/cmdlineTests/model_checker_targets_default_bmc/err‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,9 @@
1+
Warning: transfer will be deprecated in the next breaking version
2+
--> input.sol:10:3:
3+
|
4+
10 | a.transfer(x);
5+
| ^^^^^^^^^^
6+
17
Warning: BMC: Condition is always true.
28
--> input.sol:6:11:
39
|

0 commit comments

Comments
 (0)