cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

update command line tests

Browse Source
This commit is contained in:
Leonardo Alt 2021-03-31 17:31:23 +02:00
parent d89be74e4a
commit ad10bee8f0
117 changed files with 1302 additions and 1329 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
test/cmdlineTests/model_checker_engine_all/err
View File

@ -6,7 +6,7 @@ x = 0
Transaction trace:
test.constructor()
test.f(0)
--> model_checker_engine_all/input.sol:6:3:
--> model_checker_engine_all/input.sol:5:3:
|
6 | assert(x > 0);
5 | assert(x > 0);
| ^^^^^^^^^^^^^

1
test/cmdlineTests/model_checker_engine_all/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
function f(uint x) public pure {
assert(x > 0);

4
test/cmdlineTests/model_checker_engine_bmc/err
View File

@ -1,7 +1,7 @@
Warning: BMC: Assertion violation happens here.
--> model_checker_engine_bmc/input.sol:6:3:
--> model_checker_engine_bmc/input.sol:5:3:
|
6 | assert(x > 0);
5 | assert(x > 0);
| ^^^^^^^^^^^^^
Note: Counterexample:
x = 0

1
test/cmdlineTests/model_checker_engine_bmc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
function f(uint x) public pure {
assert(x > 0);

4
test/cmdlineTests/model_checker_engine_chc/err
View File

@ -6,7 +6,7 @@ x = 0
Transaction trace:
test.constructor()
test.f(0)
--> model_checker_engine_chc/input.sol:6:3:
--> model_checker_engine_chc/input.sol:5:3:
|
6 | assert(x > 0);
5 | assert(x > 0);
| ^^^^^^^^^^^^^

1
test/cmdlineTests/model_checker_engine_chc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
function f(uint x) public pure {
assert(x > 0);

1
test/cmdlineTests/model_checker_engine_none/input.sol
View File

@ -1,7 +1,6 @@
// Removed to yield a warning, otherwise CI test fails with the expectation
// "no output requested"
//pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
function f(uint x) public pure {
assert(x > 0);

2
test/cmdlineTests/model_checker_targets_all/args
View File

@ -1 +1 @@
--model-checker-targets all
--model-checker-engine all --model-checker-targets all

36
test/cmdlineTests/model_checker_targets_all/err
View File

@ -8,9 +8,9 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 0)
--> model_checker_targets_all/input.sol:8:3:
--> model_checker_targets_all/input.sol:7:3:
|
8 | --x;
7 | --x;
| ^^^
Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
@ -23,9 +23,9 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 2)
--> model_checker_targets_all/input.sol:9:3:
--> model_checker_targets_all/input.sol:8:3:
|
9 | x + type(uint).max;
8 | x + type(uint).max;
| ^^^^^^^^^^^^^^^^^^
Warning: CHC: Division by zero happens here.
@ -38,10 +38,10 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_all/input.sol:10:3:
|
10 | 2 / x;
| ^^^^^
--> model_checker_targets_all/input.sol:9:3:
|
9 | 2 / x;
| ^^^^^
Warning: CHC: Assertion violation happens here.
Counterexample:
@ -53,9 +53,9 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_all/input.sol:12:3:
--> model_checker_targets_all/input.sol:11:3:
|
12 | assert(x > 0);
11 | assert(x > 0);
| ^^^^^^^^^^^^^
Warning: CHC: Empty array "pop" happens here.
@ -68,9 +68,9 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_all/input.sol:13:3:
--> model_checker_targets_all/input.sol:12:3:
|
13 | arr.pop();
12 | arr.pop();
| ^^^^^^^^^
Warning: CHC: Out of bounds access happens here.
@ -83,22 +83,22 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_all/input.sol:14:3:
--> model_checker_targets_all/input.sol:13:3:
|
14 | arr[x];
13 | arr[x];
| ^^^^^^
Warning: BMC: Condition is always true.
--> model_checker_targets_all/input.sol:7:11:
--> model_checker_targets_all/input.sol:6:11:
|
7 | require(x >= 0);
6 | require(x >= 0);
| ^^^^^^
Note: Callstack:
Warning: BMC: Insufficient funds happens here.
--> model_checker_targets_all/input.sol:11:3:
--> model_checker_targets_all/input.sol:10:3:
|
11 | a.transfer(x);
10 | a.transfer(x);
| ^^^^^^^^^^^^^
Note: Counterexample:
a = 0

1
test/cmdlineTests/model_checker_targets_all/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

28
test/cmdlineTests/model_checker_targets_all_bmc/err
View File

@ -1,14 +1,14 @@
Warning: BMC: Condition is always true.
--> model_checker_targets_all_bmc/input.sol:7:11:
--> model_checker_targets_all_bmc/input.sol:6:11:
|
7 | require(x >= 0);
6 | require(x >= 0);
| ^^^^^^
Note: Callstack:
Warning: BMC: Underflow (resulting value less than 0) happens here.
--> model_checker_targets_all_bmc/input.sol:8:3:
--> model_checker_targets_all_bmc/input.sol:7:3:
|
8 | --x;
7 | --x;
| ^^^
Note: Counterexample:
<result> = (- 1)
@ -19,9 +19,9 @@ Note: Callstack:
Note:
Warning: BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
--> model_checker_targets_all_bmc/input.sol:9:3:
--> model_checker_targets_all_bmc/input.sol:8:3:
|
9 | x + type(uint).max;
8 | x + type(uint).max;
| ^^^^^^^^^^^^^^^^^^
Note: Counterexample:
<result> = 2**256
@ -32,10 +32,10 @@ Note: Callstack:
Note:
Warning: BMC: Division by zero happens here.
--> model_checker_targets_all_bmc/input.sol:10:3:
|
10 | 2 / x;
| ^^^^^
--> model_checker_targets_all_bmc/input.sol:9:3:
|
9 | 2 / x;
| ^^^^^
Note: Counterexample:
<result> = 0
a = 0
@ -45,9 +45,9 @@ Note: Callstack:
Note:
Warning: BMC: Insufficient funds happens here.
--> model_checker_targets_all_bmc/input.sol:11:3:
--> model_checker_targets_all_bmc/input.sol:10:3:
|
11 | a.transfer(x);
10 | a.transfer(x);
| ^^^^^^^^^^^^^
Note: Counterexample:
a = 0
@ -57,9 +57,9 @@ Note: Callstack:
Note:
Warning: BMC: Assertion violation happens here.
--> model_checker_targets_all_bmc/input.sol:12:3:
--> model_checker_targets_all_bmc/input.sol:11:3:
|
12 | assert(x > 0);
11 | assert(x > 0);
| ^^^^^^^^^^^^^
Note: Counterexample:
a = 0

1
test/cmdlineTests/model_checker_targets_all_bmc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

28
test/cmdlineTests/model_checker_targets_all_chc/err
View File

@ -8,9 +8,9 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 0)
--> model_checker_targets_all_chc/input.sol:8:3:
--> model_checker_targets_all_chc/input.sol:7:3:
|
8 | --x;
7 | --x;
| ^^^
Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
@ -23,9 +23,9 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 2)
--> model_checker_targets_all_chc/input.sol:9:3:
--> model_checker_targets_all_chc/input.sol:8:3:
|
9 | x + type(uint).max;
8 | x + type(uint).max;
| ^^^^^^^^^^^^^^^^^^
Warning: CHC: Division by zero happens here.
@ -38,10 +38,10 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_all_chc/input.sol:10:3:
|
10 | 2 / x;
| ^^^^^
--> model_checker_targets_all_chc/input.sol:9:3:
|
9 | 2 / x;
| ^^^^^
Warning: CHC: Assertion violation happens here.
Counterexample:
@ -53,9 +53,9 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_all_chc/input.sol:12:3:
--> model_checker_targets_all_chc/input.sol:11:3:
|
12 | assert(x > 0);
11 | assert(x > 0);
| ^^^^^^^^^^^^^
Warning: CHC: Empty array "pop" happens here.
@ -68,9 +68,9 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_all_chc/input.sol:13:3:
--> model_checker_targets_all_chc/input.sol:12:3:
|
13 | arr.pop();
12 | arr.pop();
| ^^^^^^^^^
Warning: CHC: Out of bounds access happens here.
@ -83,7 +83,7 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_all_chc/input.sol:14:3:
--> model_checker_targets_all_chc/input.sol:13:3:
|
14 | arr[x];
13 | arr[x];
| ^^^^^^

1
test/cmdlineTests/model_checker_targets_all_chc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

4
test/cmdlineTests/model_checker_targets_assert_bmc/err
View File

@ -1,7 +1,7 @@
Warning: BMC: Assertion violation happens here.
--> model_checker_targets_assert_bmc/input.sol:12:3:
--> model_checker_targets_assert_bmc/input.sol:11:3:
|
12 | assert(x > 0);
11 | assert(x > 0);
| ^^^^^^^^^^^^^
Note: Counterexample:
a = 0

1
test/cmdlineTests/model_checker_targets_assert_bmc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

4
test/cmdlineTests/model_checker_targets_assert_chc/err
View File

@ -8,7 +8,7 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_assert_chc/input.sol:12:3:
--> model_checker_targets_assert_chc/input.sol:11:3:
|
12 | assert(x > 0);
11 | assert(x > 0);
| ^^^^^^^^^^^^^

1
test/cmdlineTests/model_checker_targets_assert_chc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

4
test/cmdlineTests/model_checker_targets_balance_bmc/err
View File

@ -1,7 +1,7 @@
Warning: BMC: Insufficient funds happens here.
--> model_checker_targets_balance_bmc/input.sol:11:3:
--> model_checker_targets_balance_bmc/input.sol:10:3:
|
11 | a.transfer(x);
10 | a.transfer(x);
| ^^^^^^^^^^^^^
Note: Counterexample:
a = 0

1
test/cmdlineTests/model_checker_targets_balance_bmc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

1
test/cmdlineTests/model_checker_targets_balance_chc/input.sol
View File

@ -1,5 +1,4 @@
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

4
test/cmdlineTests/model_checker_targets_constant_condition_bmc/err
View File

@ -1,6 +1,6 @@
Warning: BMC: Condition is always true.
--> model_checker_targets_constant_condition_bmc/input.sol:7:11:
--> model_checker_targets_constant_condition_bmc/input.sol:6:11:
|
7 | require(x >= 0);
6 | require(x >= 0);
| ^^^^^^
Note: Callstack:

1
test/cmdlineTests/model_checker_targets_constant_condition_bmc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

1
test/cmdlineTests/model_checker_targets_constant_condition_chc/input.sol
View File

@ -1,5 +1,4 @@
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

8
test/cmdlineTests/model_checker_targets_div_by_zero_bmc/err
View File

@ -1,8 +1,8 @@
Warning: BMC: Division by zero happens here.
--> model_checker_targets_div_by_zero_bmc/input.sol:10:3:
|
10 | 2 / x;
| ^^^^^
--> model_checker_targets_div_by_zero_bmc/input.sol:9:3:
|
9 | 2 / x;
| ^^^^^
Note: Counterexample:
<result> = 0
a = 0

1
test/cmdlineTests/model_checker_targets_div_by_zero_bmc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

8
test/cmdlineTests/model_checker_targets_div_by_zero_chc/err
View File

@ -8,7 +8,7 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_div_by_zero_chc/input.sol:10:3:
|
10 | 2 / x;
| ^^^^^
--> model_checker_targets_div_by_zero_chc/input.sol:9:3:
|
9 | 2 / x;
| ^^^^^

1
test/cmdlineTests/model_checker_targets_div_by_zero_chc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

2
test/cmdlineTests/model_checker_targets_error/args
View File

@ -1 +1 @@
--model-checker-targets aaa,bbb
--model-checker-engine all --model-checker-targets aaa,bbb

1
test/cmdlineTests/model_checker_targets_error/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

1
test/cmdlineTests/model_checker_targets_out_of_bounds_bmc/input.sol
View File

@ -1,5 +1,4 @@
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

4
test/cmdlineTests/model_checker_targets_out_of_bounds_chc/err
View File

@ -8,7 +8,7 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_out_of_bounds_chc/input.sol:14:3:
--> model_checker_targets_out_of_bounds_chc/input.sol:13:3:
|
14 | arr[x];
13 | arr[x];
| ^^^^^^

1
test/cmdlineTests/model_checker_targets_out_of_bounds_chc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

4
test/cmdlineTests/model_checker_targets_overflow_bmc/err
View File

@ -1,7 +1,7 @@
Warning: BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
--> model_checker_targets_overflow_bmc/input.sol:9:3:
--> model_checker_targets_overflow_bmc/input.sol:8:3:
|
9 | x + type(uint).max;
8 | x + type(uint).max;
| ^^^^^^^^^^^^^^^^^^
Note: Counterexample:
<result> = 2**256

1
test/cmdlineTests/model_checker_targets_overflow_bmc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

4
test/cmdlineTests/model_checker_targets_overflow_chc/err
View File

@ -8,7 +8,7 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 2)
--> model_checker_targets_overflow_chc/input.sol:9:3:
--> model_checker_targets_overflow_chc/input.sol:8:3:
|
9 | x + type(uint).max;
8 | x + type(uint).max;
| ^^^^^^^^^^^^^^^^^^

1
test/cmdlineTests/model_checker_targets_overflow_chc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

1
test/cmdlineTests/model_checker_targets_pop_empty_bmc/input.sol
View File

@ -1,5 +1,4 @@
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

4
test/cmdlineTests/model_checker_targets_pop_empty_chc/err
View File

@ -8,7 +8,7 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_pop_empty_chc/input.sol:13:3:
--> model_checker_targets_pop_empty_chc/input.sol:12:3:
|
13 | arr.pop();
12 | arr.pop();
| ^^^^^^^^^

1
test/cmdlineTests/model_checker_targets_pop_empty_chc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

4
test/cmdlineTests/model_checker_targets_underflow_bmc/err
View File

@ -1,7 +1,7 @@
Warning: BMC: Underflow (resulting value less than 0) happens here.
--> model_checker_targets_underflow_bmc/input.sol:8:3:
--> model_checker_targets_underflow_bmc/input.sol:7:3:
|
8 | --x;
7 | --x;
| ^^^
Note: Counterexample:
<result> = (- 1)

1
test/cmdlineTests/model_checker_targets_underflow_bmc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

4
test/cmdlineTests/model_checker_targets_underflow_chc/err
View File

@ -8,7 +8,7 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 0)
--> model_checker_targets_underflow_chc/input.sol:8:3:
--> model_checker_targets_underflow_chc/input.sol:7:3:
|
8 | --x;
7 | --x;
| ^^^

1
test/cmdlineTests/model_checker_targets_underflow_chc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

12
test/cmdlineTests/model_checker_targets_underflow_overflow_assert_bmc/err
View File

@ -1,7 +1,7 @@
Warning: BMC: Underflow (resulting value less than 0) happens here.
--> model_checker_targets_underflow_overflow_assert_bmc/input.sol:8:3:
--> model_checker_targets_underflow_overflow_assert_bmc/input.sol:7:3:
|
8 | --x;
7 | --x;
| ^^^
Note: Counterexample:
<result> = (- 1)
@ -12,9 +12,9 @@ Note: Callstack:
Note:
Warning: BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
--> model_checker_targets_underflow_overflow_assert_bmc/input.sol:9:3:
--> model_checker_targets_underflow_overflow_assert_bmc/input.sol:8:3:
|
9 | x + type(uint).max;
8 | x + type(uint).max;
| ^^^^^^^^^^^^^^^^^^
Note: Counterexample:
<result> = 2**256
@ -25,9 +25,9 @@ Note: Callstack:
Note:
Warning: BMC: Assertion violation happens here.
--> model_checker_targets_underflow_overflow_assert_bmc/input.sol:12:3:
--> model_checker_targets_underflow_overflow_assert_bmc/input.sol:11:3:
|
12 | assert(x > 0);
11 | assert(x > 0);
| ^^^^^^^^^^^^^
Note: Counterexample:
a = 0

1
test/cmdlineTests/model_checker_targets_underflow_overflow_assert_bmc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

12
test/cmdlineTests/model_checker_targets_underflow_overflow_assert_chc/err
View File

@ -8,9 +8,9 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 0)
--> model_checker_targets_underflow_overflow_assert_chc/input.sol:8:3:
--> model_checker_targets_underflow_overflow_assert_chc/input.sol:7:3:
|
8 | --x;
7 | --x;
| ^^^
Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
@ -23,9 +23,9 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 2)
--> model_checker_targets_underflow_overflow_assert_chc/input.sol:9:3:
--> model_checker_targets_underflow_overflow_assert_chc/input.sol:8:3:
|
9 | x + type(uint).max;
8 | x + type(uint).max;
| ^^^^^^^^^^^^^^^^^^
Warning: CHC: Assertion violation happens here.
@ -38,7 +38,7 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)
--> model_checker_targets_underflow_overflow_assert_chc/input.sol:12:3:
--> model_checker_targets_underflow_overflow_assert_chc/input.sol:11:3:
|
12 | assert(x > 0);
11 | assert(x > 0);
| ^^^^^^^^^^^^^

1
test/cmdlineTests/model_checker_targets_underflow_overflow_assert_chc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

8
test/cmdlineTests/model_checker_targets_underflow_overflow_bmc/err
View File

@ -1,7 +1,7 @@
Warning: BMC: Underflow (resulting value less than 0) happens here.
--> model_checker_targets_underflow_overflow_bmc/input.sol:8:3:
--> model_checker_targets_underflow_overflow_bmc/input.sol:7:3:
|
8 | --x;
7 | --x;
| ^^^
Note: Counterexample:
<result> = (- 1)
@ -12,9 +12,9 @@ Note: Callstack:
Note:
Warning: BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
--> model_checker_targets_underflow_overflow_bmc/input.sol:9:3:
--> model_checker_targets_underflow_overflow_bmc/input.sol:8:3:
|
9 | x + type(uint).max;
8 | x + type(uint).max;
| ^^^^^^^^^^^^^^^^^^
Note: Counterexample:
<result> = 2**256

1
test/cmdlineTests/model_checker_targets_underflow_overflow_bmc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

8
test/cmdlineTests/model_checker_targets_underflow_overflow_chc/err
View File

@ -8,9 +8,9 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 0)
--> model_checker_targets_underflow_overflow_chc/input.sol:8:3:
--> model_checker_targets_underflow_overflow_chc/input.sol:7:3:
|
8 | --x;
7 | --x;
| ^^^
Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
@ -23,7 +23,7 @@ Transaction trace:
test.constructor()
State: arr = []
test.f(0, 2)
--> model_checker_targets_underflow_overflow_chc/input.sol:9:3:
--> model_checker_targets_underflow_overflow_chc/input.sol:8:3:
|
9 | x + type(uint).max;
8 | x + type(uint).max;
| ^^^^^^^^^^^^^^^^^^

1
test/cmdlineTests/model_checker_targets_underflow_overflow_chc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
uint[] arr;
function f(address payable a, uint x) public {

2
test/cmdlineTests/model_checker_timeout_all/args
View File

@ -1 +1 @@
--model-checker-timeout 1000
--model-checker-engine all --model-checker-timeout 1000

16
test/cmdlineTests/model_checker_timeout_all/err
View File

@ -1,12 +1,12 @@
Warning: CHC: Assertion violation might happen here.
--> model_checker_timeout_all/input.sol:10:3:
|
10 | assert(r % k == 0);
| ^^^^^^^^^^^^^^^^^^
--> model_checker_timeout_all/input.sol:9:3:
|
9 | assert(r % k == 0);
| ^^^^^^^^^^^^^^^^^^
Warning: BMC: Assertion violation might happen here.
--> model_checker_timeout_all/input.sol:10:3:
|
10 | assert(r % k == 0);
| ^^^^^^^^^^^^^^^^^^
--> model_checker_timeout_all/input.sol:9:3:
|
9 | assert(r % k == 0);
| ^^^^^^^^^^^^^^^^^^
Note:

1
test/cmdlineTests/model_checker_timeout_all/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
function f(uint x, uint y, uint k) public pure {
require(k > 0);

8
test/cmdlineTests/model_checker_timeout_bmc/err
View File

@ -1,6 +1,6 @@
Warning: BMC: Assertion violation might happen here.
--> model_checker_timeout_bmc/input.sol:10:3:
|
10 | assert(r % k == 0);
| ^^^^^^^^^^^^^^^^^^
--> model_checker_timeout_bmc/input.sol:9:3:
|
9 | assert(r % k == 0);
| ^^^^^^^^^^^^^^^^^^
Note:

1
test/cmdlineTests/model_checker_timeout_bmc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
function f(uint x, uint y, uint k) public pure {
require(k > 0);

8
test/cmdlineTests/model_checker_timeout_chc/err
View File

@ -1,5 +1,5 @@
Warning: CHC: Assertion violation might happen here.
--> model_checker_timeout_chc/input.sol:10:3:
|
10 | assert(r % k == 0);
| ^^^^^^^^^^^^^^^^^^
--> model_checker_timeout_chc/input.sol:9:3:
|
9 | assert(r % k == 0);
| ^^^^^^^^^^^^^^^^^^

1
test/cmdlineTests/model_checker_timeout_chc/input.sol
View File

@ -1,6 +1,5 @@
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
pragma experimental SMTChecker;
contract test {
function f(uint x, uint y, uint k) public pure {
require(k > 0);

2
test/cmdlineTests/standard_model_checker_engine_all/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract C { function f(uint x) public pure { assert(x > 0); } }"
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract C { function f(uint x) public pure { assert(x > 0); } }"
}
},
"settings":

2
test/cmdlineTests/standard_model_checker_engine_all/output.json
View File

@ -18,4 +18,4 @@ x = 0
Transaction trace:
C.constructor()
C.f(0)","severity":"warning","sourceLocation":{"end":150,"file":"A","start":137},"type":"Warning"}],"sources":{"A":{"id":0}}}
C.f(0)","severity":"warning","sourceLocation":{"end":119,"file":"A","start":106},"type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/cmdlineTests/standard_model_checker_engine_bmc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract C { function f(uint x) public pure { assert(x > 0); } }"
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract C { function f(uint x) public pure { assert(x > 0); } }"
}
},
"settings":

14
test/cmdlineTests/standard_model_checker_engine_bmc/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x890f1520a8ee68790fd3c13ddbc70536dc8afcff539c4da1a1766da6168e497e":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x944140895bd672003614580050e8349baeea7cced0d8b9447aefb6c4833b02a8":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -12,14 +12,14 @@
(declare-fun |crypto_0| () |crypto_type|)
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-fun |abi_0| () |abi_type|)
(declare-fun |x_4_0| () Int)
(declare-fun |x_3_0| () Int)
(declare-fun |expr_7_0| () Int)
(declare-fun |expr_8_0| () Int)
(declare-fun |expr_9_0| () Int)
(declare-fun |expr_10_1| () Bool)
(declare-fun |expr_9_1| () Bool)
(assert (and (and (and true true) (and (= expr_10_1 (> expr_8_0 expr_9_0)) (and (implies (and true true) true) (and (= expr_9_0 0) (and (implies (and true true) (and (>= expr_8_0 0) (<= expr_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_8_0 x_4_0) (and (and (>= x_4_0 0) (<= x_4_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))) (not expr_10_1)))
(assert (and (and (and true true) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (implies (and true true) true) (and (= expr_8_0 0) (and (implies (and true true) (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_0) (and (and (>= x_3_0 0) (<= x_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))) (not expr_9_1)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| x_4_0))
(assert (= |EVALEXPR_0| x_3_0))
(check-sat)
(get-value (|EVALEXPR_0| ))
"}},"errors":[{"component":"general","errorCode":"4661","formattedMessage":"Warning: BMC: Assertion violation happens here.
@ -35,4 +35,4 @@ Note:
","message":"BMC: Assertion violation happens here.","secondarySourceLocations":[{"message":"Counterexample:
x = 0
"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":150,"file":"A","start":137},"type":"Warning"}],"sources":{"A":{"id":0}}}
"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":119,"file":"A","start":106},"type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/cmdlineTests/standard_model_checker_engine_chc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract C { function f(uint x) public pure { assert(x > 0); } }"
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract C { function f(uint x) public pure { assert(x > 0); } }"
}
},
"settings":

2
test/cmdlineTests/standard_model_checker_engine_chc/output.json
View File

@ -18,4 +18,4 @@ x = 0
Transaction trace:
C.constructor()
C.f(0)","severity":"warning","sourceLocation":{"end":150,"file":"A","start":137},"type":"Warning"}],"sources":{"A":{"id":0}}}
C.f(0)","severity":"warning","sourceLocation":{"end":119,"file":"A","start":106},"type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/cmdlineTests/standard_model_checker_engine_none/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract C { function f(uint x) public pure { assert(x > 0); } }"
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract C { function f(uint x) public pure { assert(x > 0); } }"
}
},
"settings":

3
test/cmdlineTests/standard_model_checker_targets_all/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);
@ -23,6 +23,7 @@
{
"modelChecker":
{
"engine": "all",
"targets": "all"
}
}

136
test/cmdlineTests/standard_model_checker_targets_all/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x858035fcfc2316b3f09ebac493170a22ae2971f0f65f8ca7e125fe7f4b88756d":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x9190f95880d71b6c4636672b262f07430b161f369cc56816ad265e4fa1ee1f3a":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -13,17 +13,17 @@
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-fun |abi_0| () |abi_type|)
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_7_0| () Int)
(declare-fun |x_9_0| () Int)
(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_6_0| () Int)
(declare-fun |x_8_0| () Int)
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_0| () Int)
(declare-fun |expr_15_1| () Bool)
(declare-fun |expr_14_1| () Bool)
(assert (and (and (and true true) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) expr_15_1))
(assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) (not expr_14_1)))
(check-sat)
","0xc14e92836e07964eacd7231da77dea92406ac93d4e601c33d2300d5e067bdc1f":"(set-option :produce-models true)
","0xd32caa9b049de053b56e6d79b6b17e718634bff64ba913b2f28e5369947d4e3b":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -38,71 +38,71 @@
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-fun |abi_0| () |abi_type|)
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_7_0| () Int)
(declare-fun |x_9_0| () Int)
(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_6_0| () Int)
(declare-fun |x_8_0| () Int)
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_0| () Int)
(declare-fun |expr_15_1| () Bool)
(assert (and (and (and true true) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) (not expr_15_1)))
(check-sat)
","0xeb141c7bf753748c7972af4a35e586d579a5e374e8f2aa2455ddbdf931e5582b":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
(declare-fun |state_0| () |state_type|)
(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
(declare-fun |tx_0| () |tx_type|)
(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
(declare-fun |crypto_0| () |crypto_type|)
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-fun |abi_0| () |abi_type|)
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_7_0| () Int)
(declare-fun |x_9_0| () Int)
(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_0| () Int)
(declare-fun |expr_15_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_1| () Int)
(declare-fun |x_9_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_17_0| () Int)
(declare-fun |expr_18_1| () Int)
(declare-fun |x_8_1| () Int)
(declare-fun |expr_20_0| () Int)
(declare-fun |expr_25_1| () Int)
(declare-fun |expr_26_1| () Int)
(declare-fun |expr_27_1| () Int)
(declare-fun |expr_28_0| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_0| () Int)
(declare-fun |d_div_mod_14_0| () Int)
(declare-fun |r_div_mod_14_0| () Int)
(declare-fun |expr_31_1| () Int)
(declare-fun |expr_33_0| () Int)
(declare-fun |expr_36_0| () Int)
(declare-fun |expr_30_1| () Int)
(declare-fun |expr_32_0| () Int)
(declare-fun |expr_35_0| () Int)
(declare-fun |state_1| () |state_type|)
(declare-fun |state_2| () |state_type|)
(declare-fun |state_3| () |state_type|)
(declare-fun |expr_39_0| () Int)
(declare-fun |expr_40_0| () Int)
(declare-fun |expr_41_0| () Int)
(declare-fun |expr_42_1| () Bool)
(declare-fun |expr_45_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_50_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_51_0| () Int)
(declare-fun |expr_52_1| () Int)
(declare-fun |expr_41_1| () Bool)
(declare-fun |expr_44_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_44_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_4_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_49_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_50_0| () Int)
(declare-fun |expr_51_1| () Int)
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_36_0 0) (<= expr_36_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_36_0 x_9_1) (and (implies (and true true) (and (>= expr_33_0 0) (<= expr_33_0 1461501637330902918203684832716283019655932542975))) (and (= expr_33_0 a_7_0) (and (implies (and true true) (and (>= expr_31_1 0) (<= expr_31_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_31_1 (ite (= expr_30_0 0) 0 d_div_mod_14_0)) (and (and (<= 0 r_div_mod_14_0) (or (= expr_30_0 0) (< r_div_mod_14_0 expr_30_0))) (and (= (+ (* d_div_mod_14_0 expr_30_0) r_div_mod_14_0) expr_29_0) (and (implies (and true true) (and (>= expr_30_0 0) (<= expr_30_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_0 x_9_1) (and (implies (and true true) true) (and (= expr_29_0 2) (and (implies (and true true) (and (>= expr_27_1 0) (<= expr_27_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_27_1 (+ expr_21_0 expr_26_1)) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- expr_18_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- expr_18_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))))))))))) (< (select (|balances| state_0) this_0) expr_36_0)))
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_35_0 0) (<= expr_35_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_35_0 x_8_1) (and (implies (and true true) (and (>= expr_32_0 0) (<= expr_32_0 1461501637330902918203684832716283019655932542975))) (and (= expr_32_0 a_6_0) (and (implies (and true true) (and (>= expr_30_1 0) (<= expr_30_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_1 (ite (= expr_29_0 0) 0 d_div_mod_14_0)) (and (and (<= 0 r_div_mod_14_0) (or (= expr_29_0 0) (< r_div_mod_14_0 expr_29_0))) (and (= (+ (* d_div_mod_14_0 expr_29_0) r_div_mod_14_0) expr_28_0) (and (implies (and true true) (and (>= expr_29_0 0) (<= expr_29_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_29_0 x_8_1) (and (implies (and true true) true) (and (= expr_28_0 2) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 (+ expr_20_0 expr_25_1)) (and (implies (and true true) (and (>= expr_25_1 0) (<= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 x_8_1) (and (ite (and true true) (= x_8_1 (- expr_17_0 1)) (= x_8_1 x_8_0)) (and (implies (and true true) (and (>= expr_18_1 0) (<= expr_18_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_1 (- expr_17_0 1)) (and (implies (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))))))))))) (< (select (|balances| state_0) this_0) expr_35_0)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| a_7_0))
(assert (= |EVALEXPR_0| a_6_0))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| x_9_1))
(assert (= |EVALEXPR_1| x_8_1))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| ))
","0xdb117433a9ec32d2f491750fb369a0d49c0afb6cad5f9ea3e1739ef8b87cdf4f":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
(declare-fun |state_0| () |state_type|)
(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
(declare-fun |tx_0| () |tx_type|)
(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
(declare-fun |crypto_0| () |crypto_type|)
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-fun |abi_0| () |abi_type|)
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_6_0| () Int)
(declare-fun |x_8_0| () Int)
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_1| () Bool)
(assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) expr_14_1))
(check-sat)
"}},"errors":[{"component":"general","errorCode":"3944","formattedMessage":"Warning: CHC: Underflow (resulting value less than 0) happens here.
Counterexample:
arr = []
@ -127,7 +127,7 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 0)","severity":"warning","sourceLocation":{"end":208,"file":"A","start":205},"type":"Warning"},{"component":"general","errorCode":"4984","formattedMessage":"Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
test.f(0, 0)","severity":"warning","sourceLocation":{"end":177,"file":"A","start":174},"type":"Warning"},{"component":"general","errorCode":"4984","formattedMessage":"Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
Counterexample:
arr = []
a = 0
@ -151,7 +151,7 @@ x = 1
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 2)","severity":"warning","sourceLocation":{"end":234,"file":"A","start":216},"type":"Warning"},{"component":"general","errorCode":"4281","formattedMessage":"Warning: CHC: Division by zero happens here.
test.f(0, 2)","severity":"warning","sourceLocation":{"end":203,"file":"A","start":185},"type":"Warning"},{"component":"general","errorCode":"4281","formattedMessage":"Warning: CHC: Division by zero happens here.
Counterexample:
arr = []
a = 0
@ -175,7 +175,7 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":247,"file":"A","start":242},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
test.f(0, 1)","severity":"warning","sourceLocation":{"end":216,"file":"A","start":211},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
Counterexample:
arr = []
a = 0
@ -199,7 +199,7 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":289,"file":"A","start":276},"type":"Warning"},{"component":"general","errorCode":"2529","formattedMessage":"Warning: CHC: Empty array \"pop\" happens here.
test.f(0, 1)","severity":"warning","sourceLocation":{"end":258,"file":"A","start":245},"type":"Warning"},{"component":"general","errorCode":"2529","formattedMessage":"Warning: CHC: Empty array \"pop\" happens here.
Counterexample:
arr = []
a = 0
@ -223,7 +223,7 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":306,"file":"A","start":297},"type":"Warning"},{"component":"general","errorCode":"6368","formattedMessage":"Warning: CHC: Out of bounds access happens here.
test.f(0, 1)","severity":"warning","sourceLocation":{"end":275,"file":"A","start":266},"type":"Warning"},{"component":"general","errorCode":"6368","formattedMessage":"Warning: CHC: Out of bounds access happens here.
Counterexample:
arr = []
a = 0
@ -247,14 +247,14 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":320,"file":"A","start":314},"type":"Warning"},{"component":"general","errorCode":"6838","formattedMessage":"Warning: BMC: Condition is always true.
test.f(0, 1)","severity":"warning","sourceLocation":{"end":289,"file":"A","start":283},"type":"Warning"},{"component":"general","errorCode":"6838","formattedMessage":"Warning: BMC: Condition is always true.
--> A:7:15:
|
7 | \t\t\t\t\t\trequire(x >= 0);
| \t\t\t\t\t\t ^^^^^^
Note: Callstack:
","message":"BMC: Condition is always true.","secondarySourceLocations":[{"message":"Callstack:"}],"severity":"warning","sourceLocation":{"end":196,"file":"A","start":190},"type":"Warning"},{"component":"general","errorCode":"1236","formattedMessage":"Warning: BMC: Insufficient funds happens here.
","message":"BMC: Condition is always true.","secondarySourceLocations":[{"message":"Callstack:"}],"severity":"warning","sourceLocation":{"end":165,"file":"A","start":159},"type":"Warning"},{"component":"general","errorCode":"1236","formattedMessage":"Warning: BMC: Insufficient funds happens here.
--> A:11:7:
|
11 | \t\t\t\t\t\ta.transfer(x);
@ -269,4 +269,4 @@ Note:
","message":"BMC: Insufficient funds happens here.","secondarySourceLocations":[{"message":"Counterexample:
a = 0
x = 0
"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":268,"file":"A","start":255},"type":"Warning"}],"sources":{"A":{"id":0}}}
"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":237,"file":"A","start":224},"type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/cmdlineTests/standard_model_checker_targets_all_bmc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

388
test/cmdlineTests/standard_model_checker_targets_all_bmc/output.json
View File

File diff suppressed because one or more lines are too long

2
test/cmdlineTests/standard_model_checker_targets_all_chc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

12
test/cmdlineTests/standard_model_checker_targets_all_chc/output.json
View File

@ -22,7 +22,7 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 0)","severity":"warning","sourceLocation":{"end":208,"file":"A","start":205},"type":"Warning"},{"component":"general","errorCode":"4984","formattedMessage":"Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
test.f(0, 0)","severity":"warning","sourceLocation":{"end":177,"file":"A","start":174},"type":"Warning"},{"component":"general","errorCode":"4984","formattedMessage":"Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
Counterexample:
arr = []
a = 0
@ -46,7 +46,7 @@ x = 1
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 2)","severity":"warning","sourceLocation":{"end":234,"file":"A","start":216},"type":"Warning"},{"component":"general","errorCode":"4281","formattedMessage":"Warning: CHC: Division by zero happens here.
test.f(0, 2)","severity":"warning","sourceLocation":{"end":203,"file":"A","start":185},"type":"Warning"},{"component":"general","errorCode":"4281","formattedMessage":"Warning: CHC: Division by zero happens here.
Counterexample:
arr = []
a = 0
@ -70,7 +70,7 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":247,"file":"A","start":242},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
test.f(0, 1)","severity":"warning","sourceLocation":{"end":216,"file":"A","start":211},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
Counterexample:
arr = []
a = 0
@ -94,7 +94,7 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":289,"file":"A","start":276},"type":"Warning"},{"component":"general","errorCode":"2529","formattedMessage":"Warning: CHC: Empty array \"pop\" happens here.
test.f(0, 1)","severity":"warning","sourceLocation":{"end":258,"file":"A","start":245},"type":"Warning"},{"component":"general","errorCode":"2529","formattedMessage":"Warning: CHC: Empty array \"pop\" happens here.
Counterexample:
arr = []
a = 0
@ -118,7 +118,7 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":306,"file":"A","start":297},"type":"Warning"},{"component":"general","errorCode":"6368","formattedMessage":"Warning: CHC: Out of bounds access happens here.
test.f(0, 1)","severity":"warning","sourceLocation":{"end":275,"file":"A","start":266},"type":"Warning"},{"component":"general","errorCode":"6368","formattedMessage":"Warning: CHC: Out of bounds access happens here.
Counterexample:
arr = []
a = 0
@ -142,4 +142,4 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":320,"file":"A","start":314},"type":"Warning"}],"sources":{"A":{"id":0}}}
test.f(0, 1)","severity":"warning","sourceLocation":{"end":289,"file":"A","start":283},"type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/cmdlineTests/standard_model_checker_targets_assert_bmc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

56
test/cmdlineTests/standard_model_checker_targets_assert_bmc/output.json
View File

File diff suppressed because one or more lines are too long

2
test/cmdlineTests/standard_model_checker_targets_assert_chc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

2
test/cmdlineTests/standard_model_checker_targets_assert_chc/output.json
View File

@ -22,4 +22,4 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":289,"file":"A","start":276},"type":"Warning"}],"sources":{"A":{"id":0}}}
test.f(0, 1)","severity":"warning","sourceLocation":{"end":258,"file":"A","start":245},"type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/cmdlineTests/standard_model_checker_targets_balance_bmc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

56
test/cmdlineTests/standard_model_checker_targets_balance_bmc/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0xecb8a634d43c6b3fa690c2fec3a4763042a115cb28580d86760b27cbb849cd95":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x3b3d90fa6754444a847a9b6f723e98fc3c8b428cb56d50a010bc2c435aa1bc10":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -13,44 +13,44 @@
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-fun |abi_0| () |abi_type|)
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_7_0| () Int)
(declare-fun |x_9_0| () Int)
(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_6_0| () Int)
(declare-fun |x_8_0| () Int)
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_0| () Int)
(declare-fun |expr_15_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_1| () Int)
(declare-fun |x_9_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_17_0| () Int)
(declare-fun |expr_18_1| () Int)
(declare-fun |x_8_1| () Int)
(declare-fun |expr_20_0| () Int)
(declare-fun |expr_25_1| () Int)
(declare-fun |expr_26_1| () Int)
(declare-fun |expr_27_1| () Int)
(declare-fun |expr_28_0| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_31_1| () Int)
(declare-fun |expr_33_0| () Int)
(declare-fun |expr_36_0| () Int)
(declare-fun |expr_30_1| () Int)
(declare-fun |expr_32_0| () Int)
(declare-fun |expr_35_0| () Int)
(declare-fun |state_1| () |state_type|)
(declare-fun |state_2| () |state_type|)
(declare-fun |state_3| () |state_type|)
(declare-fun |expr_39_0| () Int)
(declare-fun |expr_40_0| () Int)
(declare-fun |expr_41_0| () Int)
(declare-fun |expr_42_1| () Bool)
(declare-fun |expr_45_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_50_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_51_0| () Int)
(declare-fun |expr_52_1| () Int)
(declare-fun |expr_41_1| () Bool)
(declare-fun |expr_44_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_44_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_4_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_49_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_50_0| () Int)
(declare-fun |expr_51_1| () Int)
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_36_0 0) (<= expr_36_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_36_0 x_9_1) (and (implies (and true true) (and (>= expr_33_0 0) (<= expr_33_0 1461501637330902918203684832716283019655932542975))) (and (= expr_33_0 a_7_0) (and (implies (and true true) (and (>= expr_31_1 0) (<= expr_31_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_31_1 (ite (= expr_30_0 0) 0 d_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_30_0 0) (< r_div_mod_0_0 expr_30_0))) (and (= (+ (* d_div_mod_0_0 expr_30_0) r_div_mod_0_0) expr_29_0) (and (implies (and true true) (and (>= expr_30_0 0) (<= expr_30_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_0 x_9_1) (and (implies (and true true) true) (and (= expr_29_0 2) (and (implies (and true true) (and (>= expr_27_1 0) (<= expr_27_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_27_1 (+ expr_21_0 expr_26_1)) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- expr_18_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- expr_18_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))))))))))) (< (select (|balances| state_0) this_0) expr_36_0)))
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_35_0 0) (<= expr_35_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_35_0 x_8_1) (and (implies (and true true) (and (>= expr_32_0 0) (<= expr_32_0 1461501637330902918203684832716283019655932542975))) (and (= expr_32_0 a_6_0) (and (implies (and true true) (and (>= expr_30_1 0) (<= expr_30_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_1 (ite (= expr_29_0 0) 0 d_div_mod_0_0)) (and (and (<= 0 r_div_mod_0_0) (or (= expr_29_0 0) (< r_div_mod_0_0 expr_29_0))) (and (= (+ (* d_div_mod_0_0 expr_29_0) r_div_mod_0_0) expr_28_0) (and (implies (and true true) (and (>= expr_29_0 0) (<= expr_29_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_29_0 x_8_1) (and (implies (and true true) true) (and (= expr_28_0 2) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 (+ expr_20_0 expr_25_1)) (and (implies (and true true) (and (>= expr_25_1 0) (<= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 x_8_1) (and (ite (and true true) (= x_8_1 (- expr_17_0 1)) (= x_8_1 x_8_0)) (and (implies (and true true) (and (>= expr_18_1 0) (<= expr_18_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_1 (- expr_17_0 1)) (and (implies (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))))))))))) (< (select (|balances| state_0) this_0) expr_35_0)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| a_7_0))
(assert (= |EVALEXPR_0| a_6_0))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| x_9_1))
(assert (= |EVALEXPR_1| x_8_1))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| ))
"}},"errors":[{"component":"general","errorCode":"1236","formattedMessage":"Warning: BMC: Insufficient funds happens here.
@ -68,4 +68,4 @@ Note:
","message":"BMC: Insufficient funds happens here.","secondarySourceLocations":[{"message":"Counterexample:
a = 0
x = 0
"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":268,"file":"A","start":255},"type":"Warning"}],"sources":{"A":{"id":0}}}
"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":237,"file":"A","start":224},"type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/cmdlineTests/standard_model_checker_targets_balance_chc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

2
test/cmdlineTests/standard_model_checker_targets_constantCondition_bmc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

34
test/cmdlineTests/standard_model_checker_targets_constantCondition_bmc/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x858035fcfc2316b3f09ebac493170a22ae2971f0f65f8ca7e125fe7f4b88756d":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x9190f95880d71b6c4636672b262f07430b161f369cc56816ad265e4fa1ee1f3a":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -13,17 +13,17 @@
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-fun |abi_0| () |abi_type|)
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_7_0| () Int)
(declare-fun |x_9_0| () Int)
(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_6_0| () Int)
(declare-fun |x_8_0| () Int)
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_0| () Int)
(declare-fun |expr_15_1| () Bool)
(declare-fun |expr_14_1| () Bool)
(assert (and (and (and true true) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) expr_15_1))
(assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) (not expr_14_1)))
(check-sat)
","0xc14e92836e07964eacd7231da77dea92406ac93d4e601c33d2300d5e067bdc1f":"(set-option :produce-models true)
","0xdb117433a9ec32d2f491750fb369a0d49c0afb6cad5f9ea3e1739ef8b87cdf4f":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -38,15 +38,15 @@
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-fun |abi_0| () |abi_type|)
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_7_0| () Int)
(declare-fun |x_9_0| () Int)
(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_6_0| () Int)
(declare-fun |x_8_0| () Int)
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_0| () Int)
(declare-fun |expr_15_1| () Bool)
(declare-fun |expr_14_1| () Bool)
(assert (and (and (and true true) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) (not expr_15_1)))
(assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) expr_14_1))
(check-sat)
"}},"errors":[{"component":"general","errorCode":"6838","formattedMessage":"Warning: BMC: Condition is always true.
--> A:7:15:
@ -55,4 +55,4 @@
| \t\t\t\t\t\t ^^^^^^
Note: Callstack:
","message":"BMC: Condition is always true.","secondarySourceLocations":[{"message":"Callstack:"}],"severity":"warning","sourceLocation":{"end":196,"file":"A","start":190},"type":"Warning"}],"sources":{"A":{"id":0}}}
","message":"BMC: Condition is always true.","secondarySourceLocations":[{"message":"Callstack:"}],"severity":"warning","sourceLocation":{"end":165,"file":"A","start":159},"type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/cmdlineTests/standard_model_checker_targets_constantCondition_chc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

2
test/cmdlineTests/standard_model_checker_targets_div_by_zero_bmc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

58
test/cmdlineTests/standard_model_checker_targets_div_by_zero_bmc/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x5b98fbb121c58b139f0f8baa8e153dfeb0a4621f789bf1cbbc586298bcae48e1":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x3d72a9e21e83263eacaad9b3eaa387b10f1219c1727796d9e946ddce1e99f5a3":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -13,46 +13,46 @@
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-fun |abi_0| () |abi_type|)
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_7_0| () Int)
(declare-fun |x_9_0| () Int)
(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_6_0| () Int)
(declare-fun |x_8_0| () Int)
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_0| () Int)
(declare-fun |expr_15_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_1| () Int)
(declare-fun |x_9_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_17_0| () Int)
(declare-fun |expr_18_1| () Int)
(declare-fun |x_8_1| () Int)
(declare-fun |expr_20_0| () Int)
(declare-fun |expr_25_1| () Int)
(declare-fun |expr_26_1| () Int)
(declare-fun |expr_27_1| () Int)
(declare-fun |expr_28_0| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_31_1| () Int)
(declare-fun |expr_33_0| () Int)
(declare-fun |expr_36_0| () Int)
(declare-fun |expr_30_1| () Int)
(declare-fun |expr_32_0| () Int)
(declare-fun |expr_35_0| () Int)
(declare-fun |state_1| () |state_type|)
(declare-fun |state_2| () |state_type|)
(declare-fun |state_3| () |state_type|)
(declare-fun |expr_39_0| () Int)
(declare-fun |expr_40_0| () Int)
(declare-fun |expr_41_0| () Int)
(declare-fun |expr_42_1| () Bool)
(declare-fun |expr_45_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_50_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_51_0| () Int)
(declare-fun |expr_52_1| () Int)
(declare-fun |expr_41_1| () Bool)
(declare-fun |expr_44_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_44_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_4_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_49_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_50_0| () Int)
(declare-fun |expr_51_1| () Int)
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_30_0 0) (<= expr_30_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_30_0 x_9_1) (and (implies (and true true) true) (and (= expr_29_0 2) (and (implies (and true true) (and (>= expr_27_1 0) (<= expr_27_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_27_1 (+ expr_21_0 expr_26_1)) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- expr_18_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- expr_18_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))) (= expr_30_0 0)))
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_29_0 0) (<= expr_29_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_29_0 x_8_1) (and (implies (and true true) true) (and (= expr_28_0 2) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 (+ expr_20_0 expr_25_1)) (and (implies (and true true) (and (>= expr_25_1 0) (<= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 x_8_1) (and (ite (and true true) (= x_8_1 (- expr_17_0 1)) (= x_8_1 x_8_0)) (and (implies (and true true) (and (>= expr_18_1 0) (<= expr_18_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_1 (- expr_17_0 1)) (and (implies (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))))))))) (= expr_29_0 0)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| a_7_0))
(assert (= |EVALEXPR_0| a_6_0))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| x_9_1))
(assert (= |EVALEXPR_1| x_8_1))
(declare-const |EVALEXPR_2| Int)
(assert (= |EVALEXPR_2| expr_30_0))
(assert (= |EVALEXPR_2| expr_29_0))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| ))
"}},"errors":[{"component":"general","errorCode":"3046","formattedMessage":"Warning: BMC: Division by zero happens here.
@ -72,4 +72,4 @@ Note:
<result> = 0
a = 0
x = 0
"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":247,"file":"A","start":242},"type":"Warning"}],"sources":{"A":{"id":0}}}
"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":216,"file":"A","start":211},"type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/cmdlineTests/standard_model_checker_targets_div_by_zero_chc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

2
test/cmdlineTests/standard_model_checker_targets_div_by_zero_chc/output.json
View File

@ -22,4 +22,4 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":247,"file":"A","start":242},"type":"Warning"}],"sources":{"A":{"id":0}}}
test.f(0, 1)","severity":"warning","sourceLocation":{"end":216,"file":"A","start":211},"type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/cmdlineTests/standard_model_checker_targets_out_of_bounds_bmc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

2
test/cmdlineTests/standard_model_checker_targets_out_of_bounds_chc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

2
test/cmdlineTests/standard_model_checker_targets_out_of_bounds_chc/output.json
View File

@ -22,4 +22,4 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":320,"file":"A","start":314},"type":"Warning"}],"sources":{"A":{"id":0}}}
test.f(0, 1)","severity":"warning","sourceLocation":{"end":289,"file":"A","start":283},"type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/cmdlineTests/standard_model_checker_targets_overflow_bmc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

58
test/cmdlineTests/standard_model_checker_targets_overflow_bmc/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0xce4156c685d481fe03752262b478cd8877739dba34535f7bfec42a2d30d45445":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x7b2c4d6761f5d49a4a2e0ba56b832d235e93abf16fe2a1383a526aa4fb4fe028":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -13,46 +13,46 @@
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-fun |abi_0| () |abi_type|)
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_7_0| () Int)
(declare-fun |x_9_0| () Int)
(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_6_0| () Int)
(declare-fun |x_8_0| () Int)
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_0| () Int)
(declare-fun |expr_15_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_1| () Int)
(declare-fun |x_9_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_17_0| () Int)
(declare-fun |expr_18_1| () Int)
(declare-fun |x_8_1| () Int)
(declare-fun |expr_20_0| () Int)
(declare-fun |expr_25_1| () Int)
(declare-fun |expr_26_1| () Int)
(declare-fun |expr_27_1| () Int)
(declare-fun |expr_28_0| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_31_1| () Int)
(declare-fun |expr_33_0| () Int)
(declare-fun |expr_36_0| () Int)
(declare-fun |expr_30_1| () Int)
(declare-fun |expr_32_0| () Int)
(declare-fun |expr_35_0| () Int)
(declare-fun |state_1| () |state_type|)
(declare-fun |state_2| () |state_type|)
(declare-fun |state_3| () |state_type|)
(declare-fun |expr_39_0| () Int)
(declare-fun |expr_40_0| () Int)
(declare-fun |expr_41_0| () Int)
(declare-fun |expr_42_1| () Bool)
(declare-fun |expr_45_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_50_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_51_0| () Int)
(declare-fun |expr_52_1| () Int)
(declare-fun |expr_41_1| () Bool)
(declare-fun |expr_44_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_44_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_4_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_49_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_50_0| () Int)
(declare-fun |expr_51_1| () Int)
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_21_0 0) (<= expr_21_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_21_0 x_9_1) (and (ite (and true true) (= x_9_1 (- expr_18_0 1)) (= x_9_1 x_9_0)) (and (implies (and true true) (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 (- expr_18_0 1)) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))) (> (+ expr_21_0 expr_26_1) 115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_25_1 0) (<= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_25_1 115792089237316195423570985008687907853269984665640564039457584007913129639935) (and (implies (and true true) (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 x_8_1) (and (ite (and true true) (= x_8_1 (- expr_17_0 1)) (= x_8_1 x_8_0)) (and (implies (and true true) (and (>= expr_18_1 0) (<= expr_18_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_1 (- expr_17_0 1)) (and (implies (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))))))))))))) (> (+ expr_20_0 expr_25_1) 115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| a_7_0))
(assert (= |EVALEXPR_0| a_6_0))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| x_9_1))
(assert (= |EVALEXPR_1| x_8_1))
(declare-const |EVALEXPR_2| Int)
(assert (= |EVALEXPR_2| (+ expr_21_0 expr_26_1)))
(assert (= |EVALEXPR_2| (+ expr_20_0 expr_25_1)))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| ))
"}},"errors":[{"component":"general","errorCode":"2661","formattedMessage":"Warning: BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
@ -72,4 +72,4 @@ Note:
<result> = 2**256
a = 0
x = 1
"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":234,"file":"A","start":216},"type":"Warning"}],"sources":{"A":{"id":0}}}
"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":203,"file":"A","start":185},"type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/cmdlineTests/standard_model_checker_targets_overflow_chc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

2
test/cmdlineTests/standard_model_checker_targets_overflow_chc/output.json
View File

@ -22,4 +22,4 @@ x = 1
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 2)","severity":"warning","sourceLocation":{"end":234,"file":"A","start":216},"type":"Warning"}],"sources":{"A":{"id":0}}}
test.f(0, 2)","severity":"warning","sourceLocation":{"end":203,"file":"A","start":185},"type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/cmdlineTests/standard_model_checker_targets_pop_empty_bmc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

2
test/cmdlineTests/standard_model_checker_targets_pop_empty_chc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

2
test/cmdlineTests/standard_model_checker_targets_pop_empty_chc/output.json
View File

@ -22,4 +22,4 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 1)","severity":"warning","sourceLocation":{"end":306,"file":"A","start":297},"type":"Warning"}],"sources":{"A":{"id":0}}}
test.f(0, 1)","severity":"warning","sourceLocation":{"end":275,"file":"A","start":266},"type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/cmdlineTests/standard_model_checker_targets_underflow_bmc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

58
test/cmdlineTests/standard_model_checker_targets_underflow_bmc/output.json
View File

@ -1,4 +1,4 @@
{"auxiliaryInputRequested":{"smtlib2queries":{"0x0a84f77238ff8229baeac139d2ec93e905d39b9dba5859a66eaeb7310243c901":"(set-option :produce-models true)
{"auxiliaryInputRequested":{"smtlib2queries":{"0x0bf4bf54fa2ecac3482de1b433e5216d0b2f9c2347e556e43c252499885165e5":"(set-option :produce-models true)
(set-logic ALL)
(declare-fun |error_0| () Int)
(declare-fun |this_0| () Int)
@ -13,46 +13,46 @@
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-fun |abi_0| () |abi_type|)
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-fun |arr_5_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_7_0| () Int)
(declare-fun |x_9_0| () Int)
(declare-fun |arr_5_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_4_length_pair_0| () |uint[]_tuple|)
(declare-fun |a_6_0| () Int)
(declare-fun |x_8_0| () Int)
(declare-fun |arr_4_length_pair_1| () |uint[]_tuple|)
(declare-fun |expr_12_0| () Int)
(declare-fun |expr_13_0| () Int)
(declare-fun |expr_14_0| () Int)
(declare-fun |expr_15_1| () Bool)
(declare-fun |expr_18_0| () Int)
(declare-fun |expr_19_1| () Int)
(declare-fun |x_9_1| () Int)
(declare-fun |expr_21_0| () Int)
(declare-fun |expr_14_1| () Bool)
(declare-fun |expr_17_0| () Int)
(declare-fun |expr_18_1| () Int)
(declare-fun |x_8_1| () Int)
(declare-fun |expr_20_0| () Int)
(declare-fun |expr_25_1| () Int)
(declare-fun |expr_26_1| () Int)
(declare-fun |expr_27_1| () Int)
(declare-fun |expr_28_0| () Int)
(declare-fun |expr_29_0| () Int)
(declare-fun |expr_30_0| () Int)
(declare-fun |d_div_mod_0_0| () Int)
(declare-fun |r_div_mod_0_0| () Int)
(declare-fun |expr_31_1| () Int)
(declare-fun |expr_33_0| () Int)
(declare-fun |expr_36_0| () Int)
(declare-fun |expr_30_1| () Int)
(declare-fun |expr_32_0| () Int)
(declare-fun |expr_35_0| () Int)
(declare-fun |state_1| () |state_type|)
(declare-fun |state_2| () |state_type|)
(declare-fun |state_3| () |state_type|)
(declare-fun |expr_39_0| () Int)
(declare-fun |expr_40_0| () Int)
(declare-fun |expr_41_0| () Int)
(declare-fun |expr_42_1| () Bool)
(declare-fun |expr_45_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_45_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_5_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_50_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_51_0| () Int)
(declare-fun |expr_52_1| () Int)
(declare-fun |expr_41_1| () Bool)
(declare-fun |expr_44_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_44_length_pair_1| () |uint[]_tuple|)
(declare-fun |arr_4_length_pair_2| () |uint[]_tuple|)
(declare-fun |expr_49_length_pair_0| () |uint[]_tuple|)
(declare-fun |expr_50_0| () Int)
(declare-fun |expr_51_1| () Int)
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_18_0 0) (<= expr_18_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_18_0 x_9_0) (and (implies (and true true) expr_15_1) (and (= expr_15_1 (>= expr_13_0 expr_14_0)) (and (implies (and true true) true) (and (= expr_14_0 0) (and (implies (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 x_9_0) (and (and (>= x_9_0 0) (<= x_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_7_0 0) (<= a_7_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_5_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))))) (< (- expr_18_0 1) 0)))
(assert (and (and (and true true) (and (implies (and true true) (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 x_8_0) (and (implies (and true true) expr_14_1) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (implies (and true true) true) (and (= expr_13_0 0) (and (implies (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint[]_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))))) (< (- expr_17_0 1) 0)))
(declare-const |EVALEXPR_0| Int)
(assert (= |EVALEXPR_0| a_7_0))
(assert (= |EVALEXPR_0| a_6_0))
(declare-const |EVALEXPR_1| Int)
(assert (= |EVALEXPR_1| x_9_0))
(assert (= |EVALEXPR_1| x_8_0))
(declare-const |EVALEXPR_2| Int)
(assert (= |EVALEXPR_2| (- expr_18_0 1)))
(assert (= |EVALEXPR_2| (- expr_17_0 1)))
(check-sat)
(get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| ))
"}},"errors":[{"component":"general","errorCode":"4144","formattedMessage":"Warning: BMC: Underflow (resulting value less than 0) happens here.
@ -72,4 +72,4 @@ Note:
<result> = (- 1)
a = 0
x = 0
"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":208,"file":"A","start":205},"type":"Warning"}],"sources":{"A":{"id":0}}}
"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":177,"file":"A","start":174},"type":"Warning"}],"sources":{"A":{"id":0}}}

2
test/cmdlineTests/standard_model_checker_targets_underflow_chc/input.json
View File

@ -4,7 +4,7 @@
{
"A":
{
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\npragma experimental SMTChecker;\ncontract test {
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;\n\ncontract test {
uint[] arr;
function f(address payable a, uint x) public {
require(x >= 0);

2
test/cmdlineTests/standard_model_checker_targets_underflow_chc/output.json
View File

@ -22,4 +22,4 @@ x = 0
Transaction trace:
test.constructor()
State: arr = []
test.f(0, 0)","severity":"warning","sourceLocation":{"end":208,"file":"A","start":205},"type":"Warning"}],"sources":{"A":{"id":0}}}
test.f(0, 0)","severity":"warning","sourceLocation":{"end":177,"file":"A","start":174},"type":"Warning"}],"sources":{"A":{"id":0}}}

Some files were not shown because too many files have changed in this diff Show More