Skip to content

Commit 3c00eb6

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

File tree

48 files changed

+590
-23
lines changed
  • test/cmdlineTests
    • model_checker_solvers_eld
    • 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.

48 files changed

+590
-23
lines changed

‎test/cmdlineTests/model_checker_solvers_eld/err‎

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
Warning: CHC: Assertion violation happens here.
2-
--> input.sol:5:3:
3-
|
4-
5 | assert(x > 0);
5-
| ^^^^^^^^^^^^^
1+
Warning: Solver Eldarica was selected for SMTChecker but it was not found in the system.
2+
3+
Warning: CHC analysis was not possible since no Horn solver was found and enabled. The accepted solvers for CHC are Eldarica and z3.

‎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 = []

0 commit comments

Comments
 (0)