diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_array_slice_2.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_array_slice_2.sol index f39576cba..69bc6a1af 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_array_slice_2.sol +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_array_slice_2.sol @@ -12,13 +12,15 @@ contract C { //assert(b1.length == b3.length); // fails for now bytes memory b4 = abi.encodePacked(data[5:10]); - assert(b1.length == b4.length); // should fail + // Disabled because of Spacer nondeterminism + //assert(b1.length == b4.length); // should fail - uint x = 5; - uint y = 10; - bytes memory b5 = abi.encodePacked(data[x:y]); + // Disabled because of Spacer nondeterminism + //uint x = 5; + //uint y = 10; + //bytes memory b5 = abi.encodePacked(data[x:y]); // should hold but the engine cannot infer that data[5:10] is fully equals data[x:y] because each index is assigned separately - assert(b1.length == b5.length); // fails for now + //assert(b1.length == b5.length); // fails for now bytes memory b6 = abi.encode(data[5:10]); assert(b4.length == b6.length); // should fail @@ -26,12 +28,4 @@ contract C { } // ---- // Warning 6328: (330-360): CHC: Assertion violation happens here. -// Warning 1218: (725-755): CHC: Error trying to invoke SMT solver. -// Warning 6328: (725-755): CHC: Assertion violation might happen here. -// Warning 1218: (982-1012): CHC: Error trying to invoke SMT solver. -// Warning 6328: (982-1012): CHC: Assertion violation might happen here. -// Warning 1218: (1078-1108): CHC: Error trying to invoke SMT solver. -// Warning 6328: (1078-1108): CHC: Assertion violation might happen here. -// Warning 4661: (725-755): BMC: Assertion violation happens here. -// Warning 4661: (982-1012): BMC: Assertion violation happens here. -// Warning 4661: (1078-1108): BMC: Assertion violation happens here. +// Warning 6328: (1182-1212): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_simple.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_simple.sol index caa8c8042..552127cbe 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_simple.sol +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_simple.sol @@ -16,8 +16,9 @@ contract C { assert(b1.length != b5.length); // should fail assert(b1.length == b5.length); // should fail - bytes memory b6 = abi.encode(x, z, a); - assert(b1.length == b6.length); // should fail + // Commented out because of nondeterminism in Spacer in Z3 4.8.9 + //bytes memory b6 = abi.encode(x, z, a); + //assert(b1.length == b6.length); // should fail } } // ---- @@ -28,7 +29,6 @@ contract C { // Warning 6328: (560-590): CHC: Assertion violation might happen here. // Warning 1218: (609-639): CHC: Error trying to invoke SMT solver. // Warning 6328: (609-639): CHC: Assertion violation might happen here. -// Warning 6328: (700-730): CHC: Assertion violation happens here. // Warning 4661: (451-481): BMC: Assertion violation happens here. // Warning 4661: (560-590): BMC: Assertion violation happens here. // Warning 4661: (609-639): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_simple.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_simple.sol index 9b3b7d185..85b249c7e 100644 --- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_simple.sol +++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_simple.sol @@ -6,8 +6,9 @@ contract C { bytes memory b2 = abi.encodeWithSignature(sig, y, z, a); assert(b1.length == b2.length); - bytes memory b3 = abi.encodeWithSignature(sig, y, z, b); - assert(b1.length == b3.length); // should fail + // Disabled because of nondeterminism in Spacer Z3 4.8.9 + //bytes memory b3 = abi.encodeWithSignature(sig, y, z, b); + //assert(b1.length == b3.length); // should fail bytes memory b4 = abi.encodeWithSignature(sig, t, z, a); assert(b1.length == b4.length); // should fail @@ -21,14 +22,10 @@ contract C { } } // ---- -// Warning 6328: (403-433): CHC: Assertion violation happens here. -// Warning 6328: (512-542): CHC: Assertion violation happens here. -// Warning 1218: (633-663): CHC: Error trying to invoke SMT solver. -// Warning 6328: (633-663): CHC: Assertion violation might happen here. -// Warning 1218: (682-712): CHC: Error trying to invoke SMT solver. -// Warning 6328: (682-712): CHC: Assertion violation might happen here. -// Warning 1218: (793-823): CHC: Error trying to invoke SMT solver. -// Warning 6328: (793-823): CHC: Assertion violation might happen here. -// Warning 4661: (633-663): BMC: Assertion violation happens here. -// Warning 4661: (682-712): BMC: Assertion violation happens here. -// Warning 4661: (793-823): BMC: Assertion violation happens here. +// Warning 5667: (139-154): Unused function parameter. Remove or comment out the variable name to silence this warning. +// Warning 6328: (575-605): CHC: Assertion violation happens here. +// Warning 6328: (696-726): CHC: Assertion violation happens here. +// Warning 6328: (745-775): CHC: Assertion violation happens here. +// Warning 1218: (856-886): CHC: Error trying to invoke SMT solver. +// Warning 6328: (856-886): CHC: Assertion violation might happen here. +// Warning 4661: (856-886): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol b/test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol index e5df8eb8a..3f8296d46 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol @@ -10,4 +10,4 @@ contract C { } } // ---- -// Warning 6328: (199-234): CHC: Assertion violation happens here.\nCounterexample:\n\na = 21238\n\n\nTransaction trace:\nconstructor()\nf(21238) +// Warning 6328: (199-234): CHC: Assertion violation happens here.\nCounterexample:\n\na = 2437\n\n\nTransaction trace:\nconstructor()\nf(2437) diff --git a/test/libsolidity/smtCheckerTests/external_calls/external.sol b/test/libsolidity/smtCheckerTests/external_calls/external.sol index 2f0b82215..b34eeae96 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external.sol @@ -17,4 +17,4 @@ contract C { } } // ---- -// Warning 6328: (200-214): CHC: Assertion violation happens here.\nCounterexample:\nx = 10, d = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0, d = 0\nf()\nState: x = 1, d = 0\nf()\nState: x = 2, d = 0\ng() +// Warning 6328: (200-214): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol index b006f4b6e..803bcd11e 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol @@ -34,4 +34,4 @@ contract C { } } // ---- -// Warning 6328: (528-565): CHC: Assertion violation happens here.\nCounterexample:\nowner = 1, y = 0, z = 0, s = 0\n\n\n\nTransaction trace:\nconstructor()\nState: owner = 1, y = 0, z = 0, s = 0\ninv() +// Warning 6328: (528-565): CHC: Assertion violation happens here.\nCounterexample:\nowner = 1, y = 0, z = 0, s = 0\n\n\n\nTransaction trace:\nconstructor()\nState: owner = 1, y = 0, z = 0, s = 0\nf() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol b/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol index 3448f1221..2e8592329 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol @@ -21,5 +21,6 @@ contract C { // SMTIgnoreCex: yes // ---- // Warning 4984: (146-149): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. +// Warning 4984: (146-149): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 6328: (189-203): CHC: Assertion violation happens here. // Warning 2661: (146-149): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_1.sol new file mode 100644 index 000000000..a2e53023e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_1.sol @@ -0,0 +1,19 @@ +pragma experimental SMTChecker; + +interface D { function e() external; } + +contract C { + bool locked = true; + + function call(address target) public { + locked = false; + D(target).e(); + locked = true; + } + + function broken() public view { + assert(locked); + } +} +// ---- +// Warning 6328: (239-253): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0\n\n\nTransaction trace:\nconstructor()\nState: locked = true\ncall(0) diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol new file mode 100644 index 000000000..8561afc2f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; + +interface D { function e() external; } + +contract C { + bool locked = true; + + function call(address target) public { + assert(locked); + locked = false; + D(target).e(); + locked = true; + } +} +// ---- +// Warning 6328: (150-164): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0\n\n\nTransaction trace:\nconstructor()\nState: locked = true\ncall(0) diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_3.sol new file mode 100644 index 000000000..c00a9d83a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_3.sol @@ -0,0 +1,31 @@ +pragma experimental SMTChecker; + +abstract contract D { + function d() virtual public {} +} + +contract A { + int x = 0; + + function f() virtual public view { + assert(x == 0); // should hold + assert(x == 1); // should fail + } +} +contract C is A { + constructor() { + x = 1; + } + + function call(D d) public { + d.d(); + } + + function f() public view override { + assert(x == 1); // should hold + assert(x == 0); // should fail + } +} +// ---- +// Warning 6328: (187-201): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf() +// Warning 6328: (385-399): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\nd = 0\n\n\nTransaction trace:\nconstructor()\nState: x = 1\ncall(0) diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol new file mode 100644 index 000000000..67af6ded7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol @@ -0,0 +1,26 @@ +pragma experimental SMTChecker; + +abstract contract D { + function d() virtual public; +} + +contract C { + bytes data; + + bytes32 kec; + + constructor(bytes memory _data) { + data = _data; + + kec = keccak256(data); + } + + function f() public view { + bytes32 _kec = keccak256(data); + assert(_kec == kec); + } + + function ext(D d) public { + d.d(); + } +} diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_state_value_inherited.sol b/test/libsolidity/smtCheckerTests/functions/constructor_state_value_inherited.sol index 1c5b62abc..100183012 100644 --- a/test/libsolidity/smtCheckerTests/functions/constructor_state_value_inherited.sol +++ b/test/libsolidity/smtCheckerTests/functions/constructor_state_value_inherited.sol @@ -15,4 +15,4 @@ contract C is B { } } // ---- -// Warning 6328: (165-179): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 11\n\n\nTransaction trace:\nconstructor()\nState: x = 10\nf(11) +// Warning 6328: (165-179): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 9\n\n\nTransaction trace:\nconstructor()\nState: x = 10\nf(9) diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol b/test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol index 24f04987e..2b2877307 100644 --- a/test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol +++ b/test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol @@ -14,4 +14,4 @@ contract C { } // ---- // Warning 6328: (162-176): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 1\n\n\nTransaction trace:\nconstructor(0, 0)\nState: x = 0\nf(1) -// Warning 4984: (115-120): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nx = 5\na = 115792089237316195423570985008687907853269984665640564039457584007913129639935\nb = 1\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639935, 1) +// Warning 4984: (115-120): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nx = 5\na = 1\nb = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\n\nTransaction trace:\nconstructor(1, 115792089237316195423570985008687907853269984665640564039457584007913129639935) diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol index b6ec5b8b1..22d8e93d6 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol @@ -12,10 +12,16 @@ contract C require(map[0] == map[1]); assert(map[0] == map[1]); d.g(y); - // Storage knowledge is cleared after an external call. assert(map[0] == map[1]); + assert(map[0] == 0); // should fail + } + + function set(uint x) public { + map[0] = x; + map[1] = x; } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (297-321): CHC: Assertion violation might happen here. -// Warning 4661: (297-321): BMC: Assertion violation happens here. +// Warning 6328: (267-286): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_2.sol index 412c70e54..5a05e9cee 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_2.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_2.sol @@ -18,5 +18,7 @@ contract C { assert(y == 1); // should fail } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (307-321): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf() +// Warning 6328: (307-321): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol index 279886553..a3faeff03 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol @@ -20,5 +20,4 @@ contract LoopFor2 { } // ---- // Warning 4984: (236-241): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. -// Warning 4984: (216-222): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 6328: (363-382): CHC: Assertion violation happens here.\nCounterexample:\nb = [], c = []\nn = 1\n\n\nTransaction trace:\nconstructor()\nState: b = [], c = []\ntestUnboundedForLoop(1) diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_string_literal.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_string_literal.sol index ef53b86f2..b4ecb7307 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_string_literal.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_string_literal.sol @@ -13,5 +13,7 @@ contract C { assert(y[0] == (bytes1("d") | bytes1("e")) ^ bytes1("f")); } } +// ==== +// SMTIgnoreCex: yes // ---- // Warning 6328: (189-208): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_5.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_5.sol index 713f407a8..938073990 100644 --- a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_5.sol +++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_5.sol @@ -24,4 +24,4 @@ contract C { } // ---- // Warning 2072: (282-288): Unused local variable. -// Warning 6328: (304-328): CHC: Assertion violation happens here.\nCounterexample:\na = false, x = 3, d = 0\n\n\n\nTransaction trace:\nconstructor()\nState: a = false, x = 0, d = 0\nf() +// Warning 6328: (304-328): CHC: Assertion violation happens here.\nCounterexample:\na = false, x = 3, d = 0\n\n = 0\n\nTransaction trace:\nconstructor()\nState: a = false, x = 0, d = 0\ng() diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol b/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol index 5c29dd5f2..d1e64336f 100644 --- a/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol +++ b/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol @@ -14,6 +14,6 @@ contract C } } // ---- -// Warning 6328: (295-324): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 100\na = 7719\nb = 7720\n\n\nTransaction trace:\nconstructor()\nf(100, 7719, 7720) +// Warning 6328: (295-324): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 100\na = 7720\nb = 7719\n\n\nTransaction trace:\nconstructor()\nf(100, 7720, 7719) // Warning 1236: (217-232): BMC: Insufficient funds happens here. // Warning 1236: (236-251): BMC: Insufficient funds happens here. diff --git a/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_5.sol b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_5.sol index 02d3d9903..f8640c93f 100644 --- a/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_5.sol +++ b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_5.sol @@ -26,5 +26,7 @@ contract C assert(b[0] == 1); } } +// ==== +// SMTIgnoreCex: yes // ---- // Warning 6328: (572-589): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/array_branch_1d.sol b/test/libsolidity/smtCheckerTests/types/array_branch_1d.sol index 40018ec36..f94c9b99f 100644 --- a/test/libsolidity/smtCheckerTests/types/array_branch_1d.sol +++ b/test/libsolidity/smtCheckerTests/types/array_branch_1d.sol @@ -2,7 +2,8 @@ pragma experimental SMTChecker; contract C { - function f(bool b, uint[] memory c) public { + function f(bool b, uint[] memory c) public pure { + require(c.length <= 2); c[0] = 0; if (b) c[0] = 1; @@ -10,5 +11,4 @@ contract C } } // ---- -// Warning 2018: (47-148): Function state mutability can be restricted to pure -// Warning 6328: (128-144): CHC: Assertion violation happens here.\nCounterexample:\n\nb = false\nc = [0, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 18, 14, 14, 21, 14, 14, 23, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14]\n\n\nTransaction trace:\nconstructor()\nf(false, [7719, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 18, 14, 14, 21, 14, 14, 23, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14]) +// Warning 6328: (159-175): CHC: Assertion violation happens here.\nCounterexample:\n\nb = false\nc = [0, 5]\n\n\nTransaction trace:\nconstructor()\nf(false, [7719, 5])