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 smtchecker tests

Browse Source
This commit is contained in:
Leo Alt 2021-11-23 18:08:36 +01:00
parent 406b1fbcec
commit ff5c842d67
53 changed files with 92 additions and 75 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
test/libsolidity/smtCheckerTests/abi/abi_decode_array.sol
View File

@ -32,9 +32,6 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 1218: (1009-1037): CHC: Error trying to invoke SMT solver.
// Warning 1218: (1056-1084): CHC: Error trying to invoke SMT solver.
// Warning 1218: (1103-1131): CHC: Error trying to invoke SMT solver.
// Warning 6328: (182-210): CHC: Assertion violation happens here.
// Warning 6328: (335-363): CHC: Assertion violation happens here.
// Warning 6328: (414-442): CHC: Assertion violation happens here.
@ -42,9 +39,6 @@ contract C {
// Warning 6328: (607-635): CHC: Assertion violation happens here.
// Warning 6328: (654-682): CHC: Assertion violation happens here.
// Warning 6328: (879-916): CHC: Assertion violation happens here.
// Warning 6328: (1009-1037): CHC: Assertion violation might happen here.
// Warning 6328: (1056-1084): CHC: Assertion violation might happen here.
// Warning 6328: (1103-1131): CHC: Assertion violation might happen here.
// Warning 4661: (1009-1037): BMC: Assertion violation happens here.
// Warning 4661: (1056-1084): BMC: Assertion violation happens here.
// Warning 4661: (1103-1131): BMC: Assertion violation happens here.
// Warning 6328: (1009-1037): CHC: Assertion violation happens here.
// Warning 6328: (1056-1084): CHC: Assertion violation happens here.
// Warning 6328: (1103-1131): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_hash.sol
View File

@ -13,9 +13,7 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (337-375): CHC: Error trying to invoke SMT solver.
// Warning 1218: (394-432): CHC: Error trying to invoke SMT solver.
// Warning 6328: (337-375): CHC: Assertion violation might happen here.
// Warning 6328: (337-375): CHC: Assertion violation happens here.
// Warning 6328: (394-432): CHC: Assertion violation might happen here.
// Warning 4661: (337-375): BMC: Assertion violation happens here.
// Warning 4661: (394-432): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol
View File

@ -31,4 +31,4 @@ contract C {
// Warning 6328: (349-375): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()
// Warning 6328: (379-402): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()
// Warning 6328: (406-432): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()
// Info 1180: Contract invariant(s) for :C:\n!(arr.length <= 3)\n!(arr.length <= 5)\n!(arr.length <= 7)\n!(arr.length <= 8)\n
// Info 1180: Contract invariant(s) for :C:\n!(arr.length <= 7)\n!(arr.length <= 8)\n

2
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol
View File

@ -18,4 +18,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (199-229): CHC: Assertion violation happens here.
// Warning 6328: (199-229): CHC: Assertion violation happens here.\nCounterexample:\nb = [1]\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.g()

2
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_1d.sol
View File

@ -14,4 +14,4 @@ contract C {
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (204-230): CHC: Assertion violation happens here.\nCounterexample:\nb = [0, 0]\nlength = 2\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.f()
// Warning 6328: (204-230): CHC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol
View File

@ -13,4 +13,3 @@ contract C {
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Info 1180: Contract invariant(s) for :C:\n(x.length >= 0)\n

4
test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2_fail.sol
View File

@ -13,5 +13,5 @@ contract C {
// SMTIgnoreOS: macos
// ----
// Warning 6328: (90-116): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[[0]]]\nlast = 0\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()
// Warning 6328: (170-186): CHC: Assertion violation happens here.
// Warning 6328: (190-246): CHC: Assertion violation happens here.
// Warning 6328: (170-186): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[[0]]]\nlast = 1\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()
// Warning 6328: (190-246): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[[0]]]\nlast = 1\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()

2
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol
View File

@ -15,7 +15,7 @@ contract C {
// Warning 4984: (82-85): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (154-160): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (212-218): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6328: (180-219): CHC: Assertion violation happens here.
// Warning 6328: (180-219): CHC: Assertion violation happens here.\nCounterexample:\nc = 1\n\nTransaction trace:\nC.constructor()\nState: c = 0\nC.f(){ msg.value: 11 }\nState: c = 1\nC.inv()
// Info 1180: Contract invariant(s) for :C:\n(((11 * c) + ((- 1) * (:var 1).balances[address(this)])) <= 0)\n
// Warning 2661: (82-85): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 2661: (154-160): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

2
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls.sol
View File

@ -15,5 +15,5 @@ contract C {
// ----
// Warning 1218: (131-165): CHC: Error trying to invoke SMT solver.
// Warning 6328: (131-165): CHC: Assertion violation might happen here.
// Info 1180: Reentrancy property(ies) for :C:\n(!(<errorCode> >= 2) && (((:var 0).balances[address(this)] + ((- 1) * (:var 1).balances[address(this)])) >= 0))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(address(this).balance == x)\n<errorCode> = 2 -> Assertion failed at assert(address(this).balance >= x)\n
// Info 1180: Reentrancy property(ies) for :C:\n(!(<errorCode> >= 2) && (((:var 1).balances[address(this)] + ((- 1) * (:var 0).balances[address(this)])) <= 0))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(address(this).balance == x)\n<errorCode> = 2 -> Assertion failed at assert(address(this).balance >= x)\n
// Warning 4661: (131-165): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_2.sol
View File

@ -12,4 +12,4 @@ contract C {
// ----
// Warning 9302: (82-93): Return value of low-level calls not used.
// Warning 6328: (97-131): CHC: Assertion violation happens here.
// Info 1180: Reentrancy property(ies) for :C:\n((((:var 1).balances[address(this)] + ((- 1) * (:var 0).balances[address(this)])) <= 0) && !(<errorCode> >= 2))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(address(this).balance == x)\n<errorCode> = 2 -> Assertion failed at assert(address(this).balance >= x)\n
// Info 1180: Reentrancy property(ies) for :C:\n(!(<errorCode> >= 2) && (((:var 1).balances[address(this)] + ((- 1) * (:var 0).balances[address(this)])) <= 0))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(address(this).balance == x)\n<errorCode> = 2 -> Assertion failed at assert(address(this).balance >= x)\n

2
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_mutex.sol
View File

@ -22,4 +22,4 @@ contract C {
// SMTIgnoreCex: yes
// ----
// Warning 6328: (277-310): CHC: Assertion violation happens here.
// Info 1180: Reentrancy property(ies) for :C:\n((!lock || (((:var 3).balances[address(this)] + ((- 1) * (:var 1).balances[address(this)])) <= 0)) && !(<errorCode> = 1) && (lock' || !lock) && (!lock || (((:var 3).balances[address(this)] + ((- 1) * (:var 1).balances[address(this)])) >= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(address(this).balance == x)\n<errorCode> = 2 -> Assertion failed at assert(address(this).balance < x)\n
// Info 1180: Reentrancy property(ies) for :C:\n((lock' || !lock) && !(<errorCode> = 1) && (!lock || (((:var 3).balances[address(this)] + ((- 1) * (:var 1).balances[address(this)])) >= 0)) && (!lock || (((:var 3).balances[address(this)] + ((- 1) * (:var 1).balances[address(this)])) <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(address(this).balance == x)\n<errorCode> = 2 -> Assertion failed at assert(address(this).balance < x)\n

2
test/libsolidity/smtCheckerTests/blockchain_state/balance_spend.sol
View File

@ -19,5 +19,5 @@ contract C {
// SMTIgnoreCex: yes
// ----
// Warning 6328: (280-314): CHC: Assertion violation happens here.
// Info 1180: Contract invariant(s) for :C:\n((!(c <= 1) || !((:var 1).balances[address(this)] <= 91)) && !((:var 1).balances[address(this)] <= 82) && (!(c <= 0) || !((:var 1).balances[address(this)] <= 100)))\n
// Info 1180: Contract invariant(s) for :C:\n((!(c <= 1) || !((:var 1).balances[address(this)] <= 90)) && !((:var 1).balances[address(this)] <= 81) && (!(c <= 0) || !((:var 1).balances[address(this)] <= 100)))\n
// Warning 1236: (175-190): BMC: Insufficient funds happens here.

1
test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol
View File

@ -16,7 +16,6 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 1218: (193-226): CHC: Error trying to invoke SMT solver.
// Warning 6328: (193-226): CHC: Assertion violation might happen here.
// Warning 6328: (245-279): CHC: Assertion violation happens here.
// Warning 6328: (298-332): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/blockchain_state/this_does_not_change_external_call.sol
View File

@ -18,4 +18,4 @@ contract C {
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Info 1180: Contract invariant(s) for :C:\n(((address(this) + ((- 1) * t)) <= 0) && ((address(this) + ((- 1) * t)) >= 0))\nReentrancy property(ies) for :C:\n((!(<errorCode> >= 2) || !((t + ((- 1) * address(this))) = 0)) && (!((t + ((- 1) * address(this))) <= 0) || ((t' + ((- 1) * address(this))) <= 0)) && (!((t + ((- 1) * address(this))) >= 0) || ((address(this) + ((- 1) * t')) <= 0)))\n(((<errorCode> <= 0) || !((t + ((- 1) * address(this))) = 0)) && (!((t + ((- 1) * address(this))) <= 0) || ((t' + ((- 1) * address(this))) <= 0)) && (!((t + ((- 1) * address(this))) >= 0) || ((address(this) + ((- 1) * t')) <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(address(this) == t)\n<errorCode> = 2 -> Assertion failed at assert(a == t)\n
// Info 1180: Contract invariant(s) for :C:\n(((address(this) + ((- 1) * t)) <= 0) && ((address(this) + ((- 1) * t)) >= 0))\nReentrancy property(ies) for :C:\n((!((t + ((- 1) * address(this))) = 0) || (<errorCode> <= 0)) && (!((t + ((- 1) * address(this))) <= 0) || ((t' + ((- 1) * address(this))) <= 0)) && (!((t + ((- 1) * address(this))) >= 0) || ((address(this) + ((- 1) * t')) <= 0)))\n((!(<errorCode> >= 2) || !((t + ((- 1) * address(this))) = 0)) && (!((t + ((- 1) * address(this))) <= 0) || ((t' + ((- 1) * address(this))) <= 0)) && (!((t + ((- 1) * address(this))) >= 0) || ((address(this) + ((- 1) * t')) <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(address(this) == t)\n<errorCode> = 2 -> Assertion failed at assert(a == t)\n

2
test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol
View File

@ -44,5 +44,5 @@ contract C {
// SMTEngine: all
// ----
// Warning 6328: (255-269): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.test()\n C.reset_if_overflow() -- internal call
// Warning 6328: (502-519): CHC: Assertion violation happens here.
// Warning 6328: (502-519): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\noldx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.set(1)\nState: x = 1\nC.test()\n C.reset_if_overflow() -- internal call
// Warning 6328: (615-629): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.set(10)\nState: x = 10\nC.test()\n C.reset_if_overflow() -- internal call

12
test/libsolidity/smtCheckerTests/crypto/crypto_functions_compare_hashes.sol
View File

@ -12,6 +12,12 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (150-164): CHC: Assertion violation happens here.
// Warning 6328: (168-182): CHC: Assertion violation happens here.
// Warning 6328: (186-200): CHC: Assertion violation happens here.
// Warning 1218: (150-164): CHC: Error trying to invoke SMT solver.
// Warning 1218: (168-182): CHC: Error trying to invoke SMT solver.
// Warning 1218: (186-200): CHC: Error trying to invoke SMT solver.
// Warning 6328: (150-164): CHC: Assertion violation might happen here.
// Warning 6328: (168-182): CHC: Assertion violation might happen here.
// Warning 6328: (186-200): CHC: Assertion violation might happen here.
// Warning 4661: (150-164): BMC: Assertion violation happens here.
// Warning 4661: (168-182): BMC: Assertion violation happens here.
// Warning 4661: (186-200): BMC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/crypto/crypto_functions_not_same.sol
View File

@ -12,4 +12,6 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (196-210): CHC: Assertion violation happens here.
// Warning 1218: (196-210): CHC: Error trying to invoke SMT solver.
// Warning 6328: (196-210): CHC: Assertion violation might happen here.
// Warning 4661: (196-210): BMC: Assertion violation happens here.

13
test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output.sol
View File

@ -37,4 +37,15 @@ contract C {
// ====
// SMTEngine: all
// ----
// Info 1180: Contract invariant(s) for :C:\n(((erc + ((- 1) * ecrecover(tuple_constructor(h, v, r, s)))) <= 0) && ((erc + ((- 1) * ecrecover(tuple_constructor(h, v, r, s)))) >= 0))\n(((kec + ((- 1) * keccak256(data))) >= 0) && ((kec + ((- 1) * keccak256(data))) <= 0))\n(((rip + ((- 1) * ripemd160(data))) <= 0) && ((rip + ((- 1) * ripemd160(data))) >= 0))\n(((sha + ((- 1) * sha256(data))) <= 0) && ((sha + ((- 1) * sha256(data))) >= 0))\n
// Warning 1218: (544-563): CHC: Error trying to invoke SMT solver.
// Warning 1218: (567-586): CHC: Error trying to invoke SMT solver.
// Warning 1218: (590-609): CHC: Error trying to invoke SMT solver.
// Warning 1218: (613-632): CHC: Error trying to invoke SMT solver.
// Warning 6328: (544-563): CHC: Assertion violation might happen here.
// Warning 6328: (567-586): CHC: Assertion violation might happen here.
// Warning 6328: (590-609): CHC: Assertion violation might happen here.
// Warning 6328: (613-632): CHC: Assertion violation might happen here.
// Warning 4661: (544-563): BMC: Assertion violation happens here.
// Warning 4661: (567-586): BMC: Assertion violation happens here.
// Warning 4661: (590-609): BMC: Assertion violation happens here.
// Warning 4661: (613-632): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/external_calls/call_mutex.sol
View File

@ -23,4 +23,4 @@ contract C {
// SMTEngine: all
// ----
// Warning 9302: (218-234): Return value of low-level calls not used.
// Info 1180: Reentrancy property(ies) for :C:\n((!lock || ((x' + ((- 1) * x)) = 0)) && (<errorCode> <= 0) && (lock' || !lock))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(y == x)\n
// Info 1180: Reentrancy property(ies) for :C:\n((lock' || !lock) && (<errorCode> <= 0) && (!lock || ((x' + ((- 1) * x)) = 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(y == x)\n

2
test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_view.sol
View File

@ -15,4 +15,4 @@ contract C {
// Warning 2519: (106-112): This declaration shadows an existing declaration.
// Warning 2072: (106-112): Unused local variable.
// Warning 2072: (114-131): Unused local variable.
// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\nReentrancy property(ies) for :C:\n((!(x <= 0) || (x' <= 0)) && ((<errorCode> <= 0) || !(x <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 0)\n
// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\nReentrancy property(ies) for :C:\n((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 0)\n

2
test/libsolidity/smtCheckerTests/external_calls/call_safe.sol
View File

@ -10,4 +10,4 @@ contract C {
// ----
// Warning 2072: (57-63): Unused local variable.
// Warning 2072: (65-82): Unused local variable.
// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\nReentrancy property(ies) for :C:\n((!(x <= 0) || (x' <= 0)) && ((<errorCode> <= 0) || !(x <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 0)\n
// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\nReentrancy property(ies) for :C:\n((!(x <= 0) || (<errorCode> <= 0)) && (!(x <= 0) || (x' <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 0)\n

4
test/libsolidity/smtCheckerTests/external_calls/call_with_value_1.sol
View File

@ -11,8 +11,6 @@ contract C {
// SMTIgnoreOS: macos
// ----
// Warning 9302: (96-117): Return value of low-level calls not used.
// Warning 1218: (175-211): CHC: Error trying to invoke SMT solver.
// Warning 6328: (121-156): CHC: Assertion violation might happen here.
// Warning 6328: (175-211): CHC: Assertion violation might happen here.
// Warning 6328: (175-211): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0x0\n\nTransaction trace:\nC.constructor()\nC.g(0x0)\n i.call{value: 10}("") -- untrusted external call
// Warning 4661: (121-156): BMC: Assertion violation happens here.
// Warning 4661: (175-211): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_1.sol
View File

@ -11,4 +11,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (157-192): CHC: Assertion violation happens here.
// Warning 6328: (157-192): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.h() -- trusted external call

2
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol
View File

@ -36,4 +36,4 @@ contract C {
// SMTIgnoreCex: yes
// ----
// Warning 6328: (495-532): CHC: Assertion violation happens here.
// Info 1180: Reentrancy property(ies) for :C:\n(((owner + ((- 1) * owner')) >= 0) && !(<errorCode> = 1) && ((owner + ((- 1) * owner')) <= 0))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(prevOwner == owner)\n<errorCode> = 3 -> Assertion failed at assert(owner == address(0) || y != z)\n
// Info 1180: Reentrancy property(ies) for :C:\n(((owner + ((- 1) * owner')) <= 0) && !(<errorCode> = 1) && ((owner + ((- 1) * owner')) >= 0))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(prevOwner == owner)\n<errorCode> = 3 -> Assertion failed at assert(owner == address(0) || y != z)\n

2
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_3.sol
View File

@ -41,4 +41,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Info 1180: Contract invariant(s) for :C:\n((insidef || (z <= 0)) && (y <= 0))\nReentrancy property(ies) for :C:\n((!insidef || !(<errorCode> >= 2)) && (!(y <= 0) || (y' <= 0)) && (insidef' || !insidef))\n((!insidef || !(<errorCode> >= 3)) && (insidef' || !insidef))\n<errorCode> = 0 -> no errors\n<errorCode> = 2 -> Assertion failed at assert(z == y)\n<errorCode> = 3 -> Assertion failed at assert(prevOwner == owner)\n
// Info 1180: Contract invariant(s) for :C:\n((insidef || (z <= 0)) && (y <= 0))\nReentrancy property(ies) for :C:\n((!insidef || !(<errorCode> >= 2)) && (insidef' || !insidef) && (!(y <= 0) || (y' <= 0)))\n((!insidef || !(<errorCode> >= 3)) && (insidef' || !insidef))\n<errorCode> = 0 -> no errors\n<errorCode> = 2 -> Assertion failed at assert(z == y)\n<errorCode> = 3 -> Assertion failed at assert(prevOwner == owner)\n

4
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe.sol
View File

@ -35,7 +35,5 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 1218: (366-392): CHC: Error trying to invoke SMT solver.
// Warning 6328: (348-362): CHC: Assertion violation happens here.
// Warning 6328: (366-392): CHC: Assertion violation might happen here.
// Warning 4661: (366-392): BMC: Assertion violation happens here.
// Warning 6328: (366-392): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_1.sol
View File

@ -16,4 +16,6 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (206-220): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0x0\n\nTransaction trace:\nC.constructor()\nState: locked = true\nC.call(0x0)\n D(target).e() -- untrusted external call, synthesized as:\n C.broken() -- reentrant call
// Warning 1218: (206-220): CHC: Error trying to invoke SMT solver.
// Warning 6328: (206-220): CHC: Assertion violation might happen here.
// Warning 4661: (206-220): BMC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol
View File

@ -27,6 +27,9 @@ contract C {
// SMTEngine: all
// SMTIgnoreInv: yes
// ----
// Warning 1218: (264-283): CHC: Error trying to invoke SMT solver.
// Warning 1218: (302-333): CHC: Error trying to invoke SMT solver.
// Warning 6328: (264-283): CHC: Assertion violation might happen here.
// Warning 6328: (302-333): CHC: Assertion violation might happen here.
// Warning 4661: (264-283): BMC: Assertion violation happens here.
// Warning 4661: (302-333): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/external_calls/external_single_inc.sol
View File

@ -23,4 +23,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (223-240): CHC: Assertion violation happens here.
// Warning 6328: (223-240): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, y = 1, d = 0\noldX = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0, d = 0\nC.inc()\nState: x = 0, y = 1, d = 0\nC.f()\n d.d() -- untrusted external call, synthesized as:\n C.inc() -- reentrant call

2
test/libsolidity/smtCheckerTests/functions/functions_external_1.sol
View File

@ -18,4 +18,4 @@ contract C
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\nReentrancy property(ies) for :C:\n!(<errorCode> = 1)\n((!(x <= 0) || !(<errorCode> >= 2)) && (!(x <= 0) || (x' <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == y)\n<errorCode> = 2 -> Assertion failed at assert(x == y)\n
// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\nReentrancy property(ies) for :C:\n!(<errorCode> = 1)\n((!(<errorCode> >= 2) || !(x <= 0)) && (!(x <= 0) || (x' <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == y)\n<errorCode> = 2 -> Assertion failed at assert(x == y)\n

2
test/libsolidity/smtCheckerTests/functions/functions_external_2.sol
View File

@ -25,4 +25,4 @@ contract C
// SMTIgnoreOS: macos
// ----
// Warning 6328: (234-253): CHC: Assertion violation happens here.
// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> = 1)\n((!((map[1] + ((- 1) * map[0])) <= 0) || ((map'[1] + ((- 1) * map'[0])) <= 0)) && !(<errorCode> = 2) && (!((map[1] + ((- 1) * map[0])) >= 0) || ((map'[0] + ((- 1) * map'[1])) <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(map[0] == map[1])\n<errorCode> = 2 -> Assertion failed at assert(map[0] == map[1])\n<errorCode> = 3 -> Assertion failed at assert(map[0] == 0)\n
// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> = 1)\n((!((map[1] + ((- 1) * map[0])) >= 0) || ((map'[0] + ((- 1) * map'[1])) <= 0)) && !(<errorCode> = 2) && (!((map[1] + ((- 1) * map[0])) <= 0) || ((map'[1] + ((- 1) * map'[0])) <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(map[0] == map[1])\n<errorCode> = 2 -> Assertion failed at assert(map[0] == map[1])\n<errorCode> = 3 -> Assertion failed at assert(map[0] == 0)\n

11
test/libsolidity/smtCheckerTests/functions/getters/struct_3.sol
View File

@ -21,5 +21,12 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (307-326): CHC: Assertion violation happens here.
// Info 1180: Contract invariant(s) for :C:\n!(m.b.length <= 2)\n
// Warning 1218: (273-277): CHC: Error trying to invoke SMT solver.
// Warning 1218: (281-287): CHC: Error trying to invoke SMT solver.
// Warning 1218: (314-318): CHC: Error trying to invoke SMT solver.
// Warning 1218: (307-326): CHC: Error trying to invoke SMT solver.
// Warning 6368: (273-277): CHC: Out of bounds access might happen here.
// Warning 6368: (281-287): CHC: Out of bounds access might happen here.
// Warning 6368: (314-318): CHC: Out of bounds access might happen here.
// Warning 6328: (307-326): CHC: Assertion violation might happen here.
// Warning 4661: (307-326): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol
View File

@ -27,4 +27,4 @@ contract C is A {
// ----
// Warning 6328: (199-214): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nA.constructor()\nState: x = 2\nA.i()
// Warning 6328: (387-401): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\n\nTransaction trace:\nC.constructor()\nState: x = 10\nC.i()
// Info 1180: Contract invariant(s) for :A:\n(!(x <= 1) && !(x >= 3))\nContract invariant(s) for :C:\n(!(x >= 11) && !(x <= 9))\n
// Info 1180: Contract invariant(s) for :A:\n(!(x <= 1) && !(x >= 3))\nContract invariant(s) for :C:\n(!(x <= 9) && !(x >= 11))\n

2
test/libsolidity/smtCheckerTests/natspec/unsafe_assert_remains_unsafe.sol
View File

@ -24,4 +24,4 @@ contract C {
// SMTEngine: chc
// ----
// Warning 6328: (74-87): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, y = 0\n_x = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(0)\n C.f1(0) -- internal call
// Warning 6328: (117-130): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, y = 0\n_x = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(0)\n C.f1(0) -- internal call\n C.f2(0) -- internal call
// Warning 6328: (117-130): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, y = 0\n_x = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(0)\n C.f1(0) -- internal call\n C.f2(0) -- internal call

2
test/libsolidity/smtCheckerTests/operators/assignment_module_contract_member_variable.sol
View File

@ -30,4 +30,4 @@ contract A {
// ----
// Warning 6328: (AASource:159-178): CHC: Assertion violation happens here.\nCounterexample:\nx = (- 1), y = (- 2)\n\nTransaction trace:\nA.constructor()\nState: x = 0, y = 0\nA.a()\nState: x = (- 2), y = (- 2)\nA.a()
// Warning 6328: (AASource:370-386): CHC: Assertion violation happens here.\nCounterexample:\nx = 8, y = (- 2)\n\nTransaction trace:\nA.constructor()\nState: x = 0, y = 0\nA.a()
// Info 1180: Contract invariant(s) for AASource:A:\n(((x = (- 2)) && (y = (- 2))) || ((x = 0) && (y = 0)))\n(((x = 0) && (y = 0)) || ((x = (- 2)) && (y = (- 2))))\n
// Info 1180: Contract invariant(s) for AASource:A:\n(((x = 0) && (y = 0)) || ((x = (- 2)) && (y = (- 2))))\n

2
test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol
View File

@ -19,4 +19,4 @@ contract C
// ====
// SMTEngine: all
// ----
// Warning 6328: (262-284): CHC: Assertion violation happens here.\nCounterexample:\narray = [200, 0]\nx = 0\np = 0\n\nTransaction trace:\nC.constructor()\nState: array = [0, 0]\nC.f(0, 0)
// Warning 6328: (262-284): CHC: Assertion violation happens here.\nCounterexample:\narray = [299, 0]\nx = 99\np = 0\n\nTransaction trace:\nC.constructor()\nState: array = [0, 0]\nC.f(99, 0)

3
test/libsolidity/smtCheckerTests/operators/compound_bitwise_string_literal_3.sol
View File

@ -18,4 +18,5 @@ contract C {
// SMTEngine: all
// ----
// Warning 6328: (229-276): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 0x6062606464666060606260646466606060626064646660606062606464666060\nz = 0x6062606464666060606260646466606060626064646660606062606464666060\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (394-437): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 0x63666566676e616263666566676e616263666566676e616263666566676e6162\nz = 0x63666566676e616263666566676e616263666566676e616263666566676e6162\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (394-437): CHC: Assertion violation might happen here.
// Warning 4661: (394-437): BMC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/operators/conditional_assignment_5.sol
View File

@ -25,6 +25,4 @@ contract C {
// SMTIgnoreCex: yes
// ----
// Warning 2072: (249-255): Unused local variable.
// Warning 1218: (271-295): CHC: Error trying to invoke SMT solver.
// Warning 6328: (271-295): CHC: Assertion violation might happen here.
// Warning 4661: (271-295): BMC: Assertion violation happens here.
// Warning 6328: (271-295): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol
View File

@ -25,4 +25,4 @@ contract C {
// SMTIgnoreOS: macos
// ----
// Warning 2072: (255-261): Unused local variable.
// Info 1180: Reentrancy property(ies) for :C:\n((!(x' <= 0) || ((x' + ((- 1) * x)) = 0)) && (<errorCode> <= 0) && (!(x' >= 3) || ((x' + ((- 1) * x)) = 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 2 || x == 1)\n
// Info 1180: Reentrancy property(ies) for :C:\n((!(x' >= 3) || (a' = a)) && (!(x' <= 0) || !(x >= 2)) && (<errorCode> <= 0) && (!(x <= 2) || !(x' >= 3)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 2 || x == 1)\n

3
test/libsolidity/smtCheckerTests/operators/slice_default_start.sol
View File

@ -11,5 +11,6 @@ contract C {
// SMTEngine: all
// ----
// Warning 6328: (150-182): CHC: Assertion violation might happen here.
// Warning 6328: (186-218): CHC: Assertion violation happens here.
// Warning 6328: (186-218): CHC: Assertion violation might happen here.
// Warning 4661: (150-182): BMC: Assertion violation happens here.
// Warning 4661: (186-218): BMC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/out_of_bounds/array_1.sol
View File

@ -21,7 +21,6 @@ contract C {
// SMTIgnoreOS: macos
// ----
// Warning 4984: (112-115): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 3944: (181-184): CHC: Underflow (resulting value less than 0) might happen here.
// Warning 6368: (259-263): CHC: Out of bounds access happens here.\nCounterexample:\na = [0], l = 1\n = 0\n\nTransaction trace:\nC.constructor()\nState: a = [], l = 0\nC.p()\nState: a = [0], l = 1\nC.r()
// Info 1180: Contract invariant(s) for :C:\n((a.length + ((- 1) * l)) <= 0)\n
// Warning 2661: (112-115): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4144: (181-184): BMC: Underflow (resulting value less than 0) happens here.

2
test/libsolidity/smtCheckerTests/overflow/unsigned_mul_overflow.sol
View File

@ -6,4 +6,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 4984: (80-85): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = 2\ny = 57896044618658097711785492504343953926634992332820282019728792003956564819968\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(2, 57896044618658097711785492504343953926634992332820282019728792003956564819968)
// Warning 4984: (80-85): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = 57896044618658097711785492504343953926634992332820282019728792003956564819968\ny = 2\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(57896044618658097711785492504343953926634992332820282019728792003956564819968, 2)

2
test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol
View File

@ -13,4 +13,4 @@ contract C {
// Warning 2072: (82-86): Unused local variable.
// Warning 2072: (140-150): Unused local variable.
// Warning 2072: (152-156): Unused local variable.
// Warning 6328: (220-236): CHC: Assertion violation happens here.\nCounterexample:\n\na1 = 2437\nb1 = 0x0a\nc1 = 9\na2 = 2437\nb2 = 0x0a\nc2 = 9\n\nTransaction trace:\nC.constructor()\nC.f(data)
// Warning 6328: (220-236): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/special/tx_vars_chc_internal.sol
View File

@ -20,4 +20,4 @@ contract C {
// ====
// SMTEngine: chc
// ----
// Warning 6328: (343-377): CHC: Assertion violation happens here.\nCounterexample:\ngas = 0, origin = 0x0\n\nTransaction trace:\nC.constructor()\nState: gas = 0, origin = 0x0\nC.f(){ tx.gasprice: 0, tx.origin: 0x0 }\n C.g() -- internal call
// Warning 6328: (343-377): CHC: Assertion violation happens here.\nCounterexample:\ngas = 0, origin = 0x52f7\n\nTransaction trace:\nC.constructor()\nState: gas = 0, origin = 0x0\nC.f(){ tx.gasprice: 0, tx.origin: 0x52f7 }\n C.g() -- internal call

2
test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol
View File

@ -13,4 +13,4 @@ contract C {
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (135-169): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 841\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 38 }\n _i.f() -- untrusted external call, synthesized as:\n C.g(0){ msg.value: 0 } -- reentrant call\n _i.f() -- untrusted external call
// Warning 6328: (135-169): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 1236\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 38 }\n _i.f() -- untrusted external call, synthesized as:\n C.g(0){ msg.value: 1 } -- reentrant call\n _i.f() -- untrusted external call

2
test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_2.sol
View File

@ -13,4 +13,4 @@ contract C {
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (157-191): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 2537\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 38 }\n _i.f{ value: 100 }() -- untrusted external call
// Warning 6328: (157-191): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 101\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 69 }\n _i.f{ value: 100 }() -- untrusted external call

2
test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol
View File

@ -21,5 +21,5 @@ contract C {
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (280-300): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (280-300): CHC: Assertion violation happens here.
// Info 1180: Contract invariant(s) for :C:\n!(m[0].length <= 1)\n(!(m[0][1] >= 43) && !(m[0][1] <= 41))\n

2
test/libsolidity/smtCheckerTests/types/abi_type_type_1.sol
View File

@ -7,4 +7,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (107-128): CHC: Assertion violation happens here.\nCounterexample:\n\na = true\nx = 1\n\nTransaction trace:\nC.constructor()\nC.f(d)
// Warning 6328: (107-128): CHC: Assertion violation happens here.

6
test/libsolidity/smtCheckerTests/types/address_staticcall.sol
View File

@ -10,7 +10,8 @@ contract C
assert(success);
assert(x == 0);
assert(map[0] == 0);
assert(localMap[0] == 0);
// Disabled because of Spacer's seg fault
//assert(localMap[0] == 0);
}
}
// ====
@ -18,6 +19,7 @@ contract C
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 2072: (127-166): Unused local variable.
// Warning 2072: (191-207): Unused local variable.
// Warning 6328: (233-248): CHC: Assertion violation happens here.
// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> >= 2)\n!(<errorCode> >= 3)\n!(<errorCode> >= 4)\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(success)\n<errorCode> = 2 -> Assertion failed at assert(x == 0)\n<errorCode> = 3 -> Assertion failed at assert(map[0] == 0)\n<errorCode> = 4 -> Assertion failed at assert(localMap[0] == 0)\n
// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> >= 2)\n!(<errorCode> >= 3)\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(success)\n<errorCode> = 2 -> Assertion failed at assert(x == 0)\n<errorCode> = 3 -> Assertion failed at assert(map[0] == 0)\n

2
test/libsolidity/smtCheckerTests/types/bool_simple_2.sol
View File

@ -6,4 +6,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (66-80): CHC: Assertion violation happens here.\nCounterexample:\n\nx = true\ny = false\n\nTransaction trace:\nC.constructor()\nC.f(true, false)
// Warning 6328: (66-80): CHC: Assertion violation happens here.\nCounterexample:\n\nx = false\ny = true\n\nTransaction trace:\nC.constructor()\nC.f(false, true)

3
test/libsolidity/smtCheckerTests/types/fixed_bytes_access_3.sol
View File

@ -32,6 +32,5 @@ contract C {
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6368: (374-381): CHC: Out of bounds access might happen here.
// Warning 6368: (456-462): CHC: Out of bounds access happens here.
// Info 1180: Contract invariant(s) for :C:\n!(a.length <= 4)\n
// Info 1180: Contract invariant(s) for :C:\n!(a.length <= 4)\n!(a[2].length <= 2)\n

2
test/libsolidity/smtCheckerTests/userTypes/user_abi_1.sol
View File

@ -11,4 +11,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (188-212): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 2437\n\nTransaction trace:\nC.constructor()\nC.f(data)
// Warning 6328: (188-212): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/userTypes/user_abi_2.sol
View File

@ -11,4 +11,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (192-226): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(data)
// Warning 6328: (192-226): CHC: Assertion violation happens here.