cerc-io/solidity
10
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 tests to z3 4.8.12

Browse Source
This commit is contained in:
Leo Alt 2021-07-15 12:13:04 +02:00
parent 3d26d47d46
commit 20e23171da
23 changed files with 29 additions and 37 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -19,15 +19,13 @@ contract C {
// ==== // ====
// SMTEngine: all // SMTEngine: all
// ---- // ----
// Warning 1218: (208-238): CHC: Error trying to invoke SMT solver. // Warning 6328: (208-238): CHC: Assertion violation happens here.
// Warning 6328: (208-238): CHC: Assertion violation might happen here.
// Warning 1218: (286-316): CHC: Error trying to invoke SMT solver. // Warning 1218: (286-316): CHC: Error trying to invoke SMT solver.
// Warning 6328: (286-316): CHC: Assertion violation might happen here. // Warning 6328: (286-316): CHC: Assertion violation might happen here.
// Warning 1218: (453-483): CHC: Error trying to invoke SMT solver. // Warning 1218: (453-483): CHC: Error trying to invoke SMT solver.
// Warning 6328: (453-483): CHC: Assertion violation might happen here. // Warning 6328: (453-483): CHC: Assertion violation might happen here.
// Warning 1218: (532-562): CHC: Error trying to invoke SMT solver. // Warning 1218: (532-562): CHC: Error trying to invoke SMT solver.
// Warning 6328: (532-562): CHC: Assertion violation might happen here. // Warning 6328: (532-562): CHC: Assertion violation might happen here.
// Warning 4661: (208-238): BMC: Assertion violation happens here.
// Warning 4661: (286-316): BMC: Assertion violation happens here. // Warning 4661: (286-316): BMC: Assertion violation happens here.
// Warning 4661: (453-483): BMC: Assertion violation happens here. // Warning 4661: (453-483): BMC: Assertion violation happens here.
// Warning 4661: (532-562): BMC: Assertion violation happens here. // Warning 4661: (532-562): BMC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_vs_sig.sol
View File

@ -9,4 +9,5 @@ contract C {
// ==== // ====
// SMTEngine: all // SMTEngine: all
// ---- // ----
// Warning 6328: (294-324): CHC: Assertion violation happens here. // Warning 6328: (294-324): CHC: Assertion violation might happen here.
// Warning 7812: (294-324): BMC: Assertion violation might happen here.

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

@ -14,5 +14,5 @@ contract C {
// SMTEngine: all // SMTEngine: all
// ---- // ----
// Warning 6368: (188-192): CHC: Out of bounds access happens here.\nCounterexample:\na = []\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f() // Warning 6368: (188-192): CHC: Out of bounds access happens here.\nCounterexample:\na = []\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 6368: (188-195): CHC: Out of bounds access happens here.\nCounterexample:\na = [[], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15]]\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f() // Warning 6368: (188-195): CHC: Out of bounds access happens here.\nCounterexample:\na = [[], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [25, 25, 25, 25, 25, 25, 25, 25], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15]]\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 6328: (181-202): CHC: Assertion violation happens here.\nCounterexample:\n\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f() // Warning 6328: (181-202): CHC: Assertion violation happens here.\nCounterexample:\n\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()

8
test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol
View File

@ -27,10 +27,6 @@ contract C {
// ---- // ----
// Warning 2072: (556-566): Unused local variable. // Warning 2072: (556-566): Unused local variable.
// Warning 2072: (598-608): Unused local variable. // Warning 2072: (598-608): Unused local variable.
// Warning 1218: (135-151): CHC: Error trying to invoke SMT solver. // Warning 6328: (135-151): CHC: Assertion violation happens here.
// Warning 6328: (135-151): CHC: Assertion violation might happen here.
// Warning 6328: (272-288): CHC: Assertion violation happens here. // Warning 6328: (272-288): CHC: Assertion violation happens here.
// Warning 1218: (415-431): CHC: Error trying to invoke SMT solver. // Warning 6328: (415-431): CHC: Assertion violation happens here.
// Warning 6328: (415-431): CHC: Assertion violation might happen here.
// Warning 4661: (135-151): BMC: Assertion violation happens here.
// Warning 4661: (415-431): BMC: Assertion violation happens here.

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

@ -20,4 +20,4 @@ contract C {
// SMTEngine: all // SMTEngine: all
// ---- // ----
// Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100) // Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100)
// Warning 6328: (203-217): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 3\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 3\nC.f() // Warning 6328: (203-217): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 0\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 0\nC.f()

2
test/libsolidity/smtCheckerTests/file_level/constants_at_file_level_referencing.sol
View File

@ -58,7 +58,7 @@ contract C {
// ==== // ====
// SMTEngine: all // SMTEngine: all
// ---- // ----
// Warning 6328: (s2.sol:518-539): CHC: Assertion violation happens here.\nCounterexample:\n\nr1 = [3, 1, 2]\nr2 = []\nr3 = []\nz = 0\n\nTransaction trace:\nC.constructor()\nC.p()\n C.f() -- internal call // Warning 6328: (s2.sol:518-539): CHC: Assertion violation happens here.\nCounterexample:\n\nr2 = []\nr3 = []\nz = 0\n\nTransaction trace:\nC.constructor()\nC.p()\n C.f() -- internal call
// Warning 6328: (s2.sol:704-725): CHC: Assertion violation happens here.\nCounterexample:\n\nr1 = [3, 1, 2]\nr2 = [3, 1, 2]\nr3 = []\nz = 0\n\nTransaction trace:\nC.constructor()\nC.p()\n C.f() -- internal call\n C.g() -- internal call // Warning 6328: (s2.sol:704-725): CHC: Assertion violation happens here.\nCounterexample:\n\nr1 = [3, 1, 2]\nr2 = [3, 1, 2]\nr3 = []\nz = 0\n\nTransaction trace:\nC.constructor()\nC.p()\n C.f() -- internal call\n C.g() -- internal call
// Warning 6328: (s2.sol:890-911): CHC: Assertion violation happens here. // Warning 6328: (s2.sol:890-911): CHC: Assertion violation happens here.
// Warning 6328: (s2.sol:980-994): CHC: Assertion violation happens here. // Warning 6328: (s2.sol:980-994): CHC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/file_level/free_function_1.sol
View File

@ -12,4 +12,4 @@ function fun(uint[] calldata _x, uint[] storage _y) view returns (uint, uint[]
// SMTEngine: all // SMTEngine: all
// ---- // ----
// Warning 4984: (168-180): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\ndata = []\nx = 1\n = 0\n = 0\na = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(1, input)\n fun(_x, []) -- internal call // Warning 4984: (168-180): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\ndata = []\nx = 1\n = 0\n = 0\na = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(1, input)\n fun(_x, []) -- internal call
// Warning 6368: (289-294): CHC: Out of bounds access happens here.\nCounterexample:\ndata = []\nx = 0\ninput = [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5]\n = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(0, [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5])\n fun([5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5], []) -- internal call // Warning 6368: (289-294): CHC: Out of bounds access happens here.\nCounterexample:\ndata = []\nx = 0\ninput = [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 5, 5, 5, 16, 5, 5, 20, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5]\n = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(0, [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 5, 5, 5, 16, 5, 5, 20, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5])\n fun([5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 5, 5, 5, 16, 5, 5, 20, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5], []) -- internal call

2
test/libsolidity/smtCheckerTests/file_level/libraries_from_free.sol
View File

@ -23,6 +23,6 @@ contract C {
// ---- // ----
// Warning 4588: (190-197): Assertion checker does not yet implement this type of function call. // Warning 4588: (190-197): Assertion checker does not yet implement this type of function call.
// Warning 4588: (190-197): Assertion checker does not yet implement this type of function call. // Warning 4588: (190-197): Assertion checker does not yet implement this type of function call.
// Warning 6328: (284-298): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 8\ny = 8\n\nTransaction trace:\nC.constructor()\nC.f()\n fu() -- internal call\n L.inter() -- internal call // Warning 6328: (284-298): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 8\n\nTransaction trace:\nC.constructor()\nC.f()\n fu() -- internal call\n L.inter() -- internal call
// Warning 6328: (363-377): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 8\n\nTransaction trace:\nC.constructor()\nC.f()\n fu() -- internal call\n L.inter() -- internal call // Warning 6328: (363-377): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 8\n\nTransaction trace:\nC.constructor()\nC.f()\n fu() -- internal call\n L.inter() -- internal call
// Warning 4588: (190-197): Assertion checker does not yet implement this type of function call. // Warning 4588: (190-197): Assertion checker does not yet implement this type of function call.

6
test/libsolidity/smtCheckerTests/file_level/recursion.sol
View File

@ -26,14 +26,16 @@ contract C {
// Warning 4281: (118-130): CHC: Division by zero might happen here. // Warning 4281: (118-130): CHC: Division by zero might happen here.
// Warning 4984: (134-148): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 4984: (134-148): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (176-189): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 4984: (176-189): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6328: (430-450): CHC: Assertion violation happens here. // Warning 6328: (430-450): CHC: Assertion violation might happen here.
// Warning 6328: (454-474): CHC: Assertion violation might happen here.
// Warning 6328: (478-498): CHC: Assertion violation might happen here. // Warning 6328: (478-498): CHC: Assertion violation might happen here.
// Warning 6328: (502-527): CHC: Assertion violation might happen here. // Warning 6328: (502-527): CHC: Assertion violation might happen here.
// Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 2661: (176-189): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 2661: (176-189): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4661: (454-474): BMC: Assertion violation happens here.
// Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 8065: (176-189): BMC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 2661: (176-189): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4661: (478-498): BMC: Assertion violation happens here. // Warning 4661: (478-498): BMC: Assertion violation happens here.
// Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4661: (502-527): BMC: Assertion violation happens here. // Warning 4661: (502-527): BMC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/functions/getters/bytes.sol
View File

@ -10,6 +10,4 @@ contract C {
// ==== // ====
// SMTEngine: all // SMTEngine: all
// ---- // ----
// Warning 1218: (162-201): CHC: Error trying to invoke SMT solver. // Warning 6328: (162-201): CHC: Assertion violation happens here.
// Warning 6328: (162-201): CHC: Assertion violation might happen here.
// Warning 4661: (162-201): BMC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/functions/getters/string.sol
View File

@ -10,6 +10,4 @@ contract C {
// ==== // ====
// SMTEngine: all // SMTEngine: all
// ---- // ----
// Warning 1218: (178-224): CHC: Error trying to invoke SMT solver. // Warning 6328: (178-224): CHC: Assertion violation happens here.
// Warning 6328: (178-224): CHC: Assertion violation might happen here.
// Warning 4661: (178-224): BMC: Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/loops/while_nested_break_fail.sol
View File

@ -30,4 +30,4 @@ contract C
// SMTEngine: all // SMTEngine: all
// ---- // ----
// Warning 6328: (296-311): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 10\nb = false\nc = true\n\nTransaction trace:\nC.constructor()\nC.f(0, 9, false, true) // Warning 6328: (296-311): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 10\nb = false\nc = true\n\nTransaction trace:\nC.constructor()\nC.f(0, 9, false, true)
// Warning 6328: (347-362): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 15\ny = 20\nb = false\nc = false\n\nTransaction trace:\nC.constructor()\nC.f(0, 0, false, false) // Warning 6328: (347-362): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 15\ny = 0\nb = true\nc = false\n\nTransaction trace:\nC.constructor()\nC.f(9, 0, true, false)

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

@ -33,11 +33,9 @@ contract C {
// ==== // ====
// SMTEngine: chc // SMTEngine: chc
// ---- // ----
// Warning 4984: (176-179): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4281: (435-447): CHC: Division by zero might happen here. // Warning 4281: (435-447): CHC: Division by zero might happen here.
// Warning 4984: (467-478): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 4984: (467-478): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4281: (495-507): CHC: Division by zero might happen here. // Warning 4281: (495-507): CHC: Division by zero might happen here.
// Warning 4984: (529-537): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 4984: (529-537): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (550-561): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 4984: (550-561): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 3944: (579-591): CHC: Underflow (resulting value less than 0) might happen here.
// Warning 4984: (616-624): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 4984: (616-624): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.

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

@ -26,4 +26,4 @@ contract C {
// ---- // ----
// Warning 2018: (33-335): Function state mutability can be restricted to view // Warning 2018: (33-335): Function state mutability can be restricted to view
// Warning 2018: (457-524): Function state mutability can be restricted to pure // Warning 2018: (457-524): Function state mutability can be restricted to pure
// Warning 6328: (135-150): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, y = 0\n_x = 0\nz = 1\nt = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(0)\n C.f1(0) -- internal call // Warning 6328: (135-150): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, y = 0\n_x = 1\nz = 0\nt = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(1)\n C.f1(1) -- internal call

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

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

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

@ -6,4 +6,4 @@ contract C {
// ==== // ====
// SMTEngine: all // SMTEngine: all
// ---- // ----
// 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) // 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)

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

@ -15,6 +15,6 @@ contract C {
// Warning 2072: (152-156): Unused local variable. // Warning 2072: (152-156): Unused local variable.
// Warning 8364: (123-124): Assertion checker does not yet implement type type(contract C) // Warning 8364: (123-124): Assertion checker does not yet implement type type(contract C)
// Warning 8364: (193-194): Assertion checker does not yet implement type type(contract C) // Warning 8364: (193-194): Assertion checker does not yet implement type type(contract C)
// Warning 6328: (220-236): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [13, 13, 13, 13, 13, 13, 13, 13, 10, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13]\na1 = 7719\nb1 = 5\nc1 = 6\na2 = 7719\nb2 = 5\nc2 = 6\n\nTransaction trace:\nC.constructor()\nC.f([13, 13, 13, 13, 13, 13, 13, 13, 10, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13]) // Warning 6328: (220-236): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 13, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9]\na1 = 7719\nb1 = 5\nc1 = 6\na2 = 7719\nb2 = 5\nc2 = 6\n\nTransaction trace:\nC.constructor()\nC.f([9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 13, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9])
// Warning 8364: (123-124): Assertion checker does not yet implement type type(contract C) // Warning 8364: (123-124): Assertion checker does not yet implement type type(contract C)
// Warning 8364: (193-194): Assertion checker does not yet implement type type(contract C) // Warning 8364: (193-194): Assertion checker does not yet implement type type(contract C)

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

@ -11,4 +11,4 @@ contract C
// SMTEngine: all // SMTEngine: all
// ---- // ----
// Warning 6328: (52-76): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f(38){ value: 8365 } // Warning 6328: (52-76): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f(38){ value: 8365 }
// Warning 6328: (80-104): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f(38){ value: 32285 } // Warning 6328: (80-104): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f(38){ value: 5853 }

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

@ -27,4 +27,4 @@ contract C {
// ---- // ----
// Warning 6321: (247-251): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. // Warning 6321: (247-251): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable.
// Warning 6321: (397-401): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable. // Warning 6321: (397-401): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable.
// Warning 6328: (407-416): CHC: Assertion violation happens here.\nCounterexample:\nx = false\n\nTransaction trace:\nC.constructor()\nState: x = true\nC.h()\n C.h_data() -- internal call\n C.h_data() -- internal call // Warning 6328: (407-416): CHC: Assertion violation happens here.\nCounterexample:\nx = false\n\nTransaction trace:\nC.constructor()\nState: x = true\nC.h()\n C.h_data() -- internal call

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

@ -23,4 +23,4 @@ contract C
// SMTEngine: all // SMTEngine: all
// ---- // ----
// Warning 6328: (120-147): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(){ value: 30612 } // Warning 6328: (120-147): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(){ value: 30612 }
// Warning 6328: (467-494): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g(){ value: 30612 } // Warning 6328: (467-494): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g(){ value: 11797 }

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

@ -20,4 +20,4 @@ contract C {
// ==== // ====
// SMTEngine: all // SMTEngine: all
// ---- // ----
// Warning 6328: (306-320): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 3\nsuccess = false\n\nTransaction trace:\nC.constructor()\nC.f() // Warning 6328: (306-320): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\nsuccess = false\n\nTransaction trace:\nC.constructor()\nC.f()

1
test/libsolidity/smtCheckerTests/types/array_aliasing_storage_5.sol
View File

@ -33,6 +33,7 @@ contract C
// SMTEngine: all // SMTEngine: all
// SMTIgnoreCex: yes // SMTIgnoreCex: yes
// ---- // ----
// Warning 6368: (186-196): CHC: Out of bounds access might happen here.
// Warning 6368: (329-333): CHC: Out of bounds access happens here. // Warning 6368: (329-333): CHC: Out of bounds access happens here.
// Warning 6368: (342-346): CHC: Out of bounds access happens here. // Warning 6368: (342-346): CHC: Out of bounds access happens here.
// Warning 6368: (355-359): CHC: Out of bounds access happens here. // Warning 6368: (355-359): CHC: Out of bounds access happens here.

6
test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_unsafe_1.sol
View File

@ -41,8 +41,8 @@ contract C {
// ==== // ====
// SMTEngine: all // SMTEngine: all
// ---- // ----
// Warning 6328: (148-165): CHC: Assertion violation happens here. // Warning 6328: (148-165): CHC: Assertion violation happens here.\nCounterexample:\ns1 = {x: 2, t: {y: 0, a: []}, a: [], ts: []}\n\nTransaction trace:\nC.constructor()\nState: s1 = {x: 0, t: {y: 0, a: []}, a: [], ts: []}\nC.f()
// Warning 6328: (183-202): CHC: Assertion violation happens here.\nCounterexample:\ns1 = {x: 2, t: {y: 3, a: []}, a: [], ts: []}\n\nTransaction trace:\nC.constructor()\nState: s1 = {x: 0, t: {y: 0, a: []}, a: [], ts: []}\nC.f() // Warning 6328: (183-202): CHC: Assertion violation happens here.
// Warning 6328: (266-286): CHC: Assertion violation happens here. // Warning 6328: (266-286): CHC: Assertion violation happens here.
// Warning 6328: (404-427): CHC: Assertion violation happens here.\nCounterexample:\ns1 = {x: 2, t: {y: 3, a: []}, a: [0, 0, 4], ts: [{y: 0, a: []}, {y: 0, a: []}, {y: 0, a: []}, {y: 5, a: []}, {y: 0, a: []}, {y: 0, a: []}]}\n\nTransaction trace:\nC.constructor()\nState: s1 = {x: 0, t: {y: 0, a: []}, a: [], ts: []}\nC.f() // Warning 6328: (404-427): CHC: Assertion violation happens here.\nCounterexample:\ns1 = {x: 2, t: {y: 3, a: []}, a: [0, 0, 4], ts: [{y: 0, a: []}, {y: 0, a: []}, {y: 0, a: []}, {y: 5, a: []}, {y: 0, a: []}, {y: 0, a: []}]}\n\nTransaction trace:\nC.constructor()\nState: s1 = {x: 0, t: {y: 0, a: []}, a: [], ts: []}\nC.f()
// Warning 6328: (578-604): CHC: Assertion violation happens here.\nCounterexample:\ns1 = {x: 2, t: {y: 3, a: []}, a: [0, 0, 4], ts: [{y: 0, a: []}, {y: 0, a: []}, {y: 0, a: []}, {y: 5, a: []}, {y: 0, a: [0, 0, 0, 0, 0, 6]}, {y: 0, a: []}]}\n\nTransaction trace:\nC.constructor()\nState: s1 = {x: 0, t: {y: 0, a: []}, a: [], ts: []}\nC.f() // Warning 6328: (578-604): CHC: Assertion violation happens here.