Skip to content

Commit cb21835

Browse files
matheusaaguiarmatheusaaguiar
committed
Update cmdline tests
1 parent a347803 commit cb21835

File tree

50 files changed

+602
-0
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_constant_condition_chc
    • 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_bmc
    • model_checker_targets_out_of_bounds_chc
    • model_checker_targets_overflow_bmc
    • model_checker_targets_overflow_chc
    • model_checker_targets_pop_empty_bmc
    • 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.

50 files changed

+602
-0
lines changed

‎test/cmdlineTests/model_checker_targets_all_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: Underflow (resulting value less than 0) happens here.
28
Counterexample:
39
arr = []

‎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 & 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: Underflow (resulting value less than 0) happens here.
28
Counterexample:
39
arr = []

‎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_constant_condition_chc/err‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
Warning: transfer will be deprecated in the next breaking version.
2+
--> input.sol:11:3:
3+
|
4+
11 | a.transfer(x);
5+
| ^^^^^^^^^^

‎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)