cerc-io/solidity
15
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 existing tests

Browse Source
This commit is contained in:
Leo Alt 2021-08-20 18:47:30 +02:00
parent 563469ac33
commit 85378b1770
68 changed files with 177 additions and 95 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

@ -45,6 +45,9 @@ contract C {
// Warning 8364: (779-789): Assertion checker does not yet implement type type(uint256[] memory[] memory[] memory)
// Warning 8364: (989-995): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (997-1003): Assertion checker does not yet implement type type(uint256[] memory)
// 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.
@ -52,9 +55,9 @@ 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 happens here.
// Warning 6328: (1056-1084): CHC: Assertion violation happens here.
// Warning 6328: (1103-1131): 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 8364: (162-168): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (170-176): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (283-289): Assertion checker does not yet implement type type(uint256[] memory)
@ -69,3 +72,6 @@ contract C {
// Warning 8364: (779-789): Assertion checker does not yet implement type type(uint256[] memory[] memory[] memory)
// Warning 8364: (989-995): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (997-1003): Assertion checker does not yet implement type type(uint256[] memory)
// 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.

8
test/libsolidity/smtCheckerTests/abi/abi_decode_simple.sol
View File

@ -21,10 +21,14 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 1218: (505-519): CHC: Error trying to invoke SMT solver.
// Warning 1218: (538-552): CHC: Error trying to invoke SMT solver.
// Warning 6328: (209-223): CHC: Assertion violation happens here.
// Warning 6328: (260-274): CHC: Assertion violation happens here.
// Warning 6328: (359-373): CHC: Assertion violation happens here.
// Warning 6328: (392-406): CHC: Assertion violation happens here.
// Warning 6328: (425-434): CHC: Assertion violation happens here.
// Warning 6328: (505-519): CHC: Assertion violation happens here.
// Warning 6328: (538-552): CHC: Assertion violation happens here.
// Warning 6328: (505-519): CHC: Assertion violation might happen here.
// Warning 6328: (538-552): CHC: Assertion violation might happen here.
// Warning 4661: (505-519): BMC: Assertion violation happens here.
// Warning 4661: (538-552): BMC: Assertion violation happens here.

16
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_simple.sol
View File

@ -23,7 +23,15 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (322-352): CHC: Assertion violation happens here.
// Warning 6328: (419-449): CHC: Assertion violation happens here.
// Warning 6328: (528-558): CHC: Assertion violation happens here.
// Warning 6328: (577-607): CHC: Assertion violation happens here.
// Warning 1218: (322-352): CHC: Error trying to invoke SMT solver.
// Warning 1218: (419-449): CHC: Error trying to invoke SMT solver.
// Warning 1218: (528-558): CHC: Error trying to invoke SMT solver.
// Warning 1218: (577-607): CHC: Error trying to invoke SMT solver.
// Warning 6328: (322-352): CHC: Assertion violation might happen here.
// Warning 6328: (419-449): CHC: Assertion violation might happen here.
// Warning 6328: (528-558): CHC: Assertion violation might happen here.
// Warning 6328: (577-607): CHC: Assertion violation might happen here.
// Warning 4661: (322-352): BMC: Assertion violation happens here.
// Warning 4661: (419-449): BMC: Assertion violation happens here.
// Warning 4661: (528-558): BMC: Assertion violation happens here.
// Warning 4661: (577-607): BMC: Assertion violation happens here.

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

@ -22,15 +22,17 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (226-256): CHC: Error trying to invoke SMT solver.
// Warning 1218: (310-340): CHC: Error trying to invoke SMT solver.
// Warning 1218: (483-513): CHC: Error trying to invoke SMT solver.
// Warning 1218: (568-598): CHC: Error trying to invoke SMT solver.
// Warning 1218: (654-684): CHC: Error trying to invoke SMT solver.
// Warning 6328: (226-256): CHC: Assertion violation happens here.
// Warning 6328: (226-256): CHC: Assertion violation might happen here.
// Warning 6328: (310-340): CHC: Assertion violation might happen here.
// Warning 6328: (483-513): CHC: Assertion violation might happen here.
// Warning 6328: (568-598): CHC: Assertion violation might happen here.
// Warning 6328: (654-684): CHC: Assertion violation might happen here.
// Warning 4661: (226-256): BMC: Assertion violation happens here.
// Warning 4661: (310-340): BMC: Assertion violation happens here.
// Warning 4661: (483-513): BMC: Assertion violation happens here.
// Warning 4661: (568-598): BMC: Assertion violation happens here.

5
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal_no_unproved.sol
View File

@ -23,12 +23,13 @@ contract C {
// SMTEngine: all
// SMTShowUnproved: no
// ----
// Warning 1218: (226-256): CHC: Error trying to invoke SMT solver.
// Warning 1218: (310-340): CHC: Error trying to invoke SMT solver.
// Warning 1218: (483-513): CHC: Error trying to invoke SMT solver.
// Warning 1218: (568-598): CHC: Error trying to invoke SMT solver.
// Warning 1218: (654-684): CHC: Error trying to invoke SMT solver.
// Warning 6328: (226-256): CHC: Assertion violation happens here.
// Warning 5840: CHC: 4 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
// Warning 5840: CHC: 5 verification condition(s) could not be proved. Enable the model checker option "show unproved" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
// Warning 4661: (226-256): BMC: Assertion violation happens here.
// Warning 4661: (310-340): BMC: Assertion violation happens here.
// Warning 4661: (483-513): BMC: Assertion violation happens here.
// Warning 4661: (568-598): BMC: Assertion violation happens here.

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

@ -20,6 +20,12 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (298-328): CHC: Assertion violation happens here.
// Warning 6328: (389-419): CHC: Assertion violation happens here.
// Warning 6328: (492-522): CHC: Assertion violation happens here.
// Warning 1218: (298-328): CHC: Error trying to invoke SMT solver.
// Warning 1218: (389-419): CHC: Error trying to invoke SMT solver.
// Warning 1218: (492-522): CHC: Error trying to invoke SMT solver.
// Warning 6328: (298-328): CHC: Assertion violation might happen here.
// Warning 6328: (389-419): CHC: Assertion violation might happen here.
// Warning 6328: (492-522): CHC: Assertion violation might happen here.
// Warning 4661: (298-328): BMC: Assertion violation happens here.
// Warning 4661: (389-419): BMC: Assertion violation happens here.
// Warning 4661: (492-522): BMC: Assertion violation happens here.

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

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

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

@ -25,14 +25,16 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (578-608): CHC: Error trying to invoke SMT solver.
// Warning 1218: (691-721): CHC: Error trying to invoke SMT solver.
// Warning 1218: (959-989): CHC: Error trying to invoke SMT solver.
// Warning 1218: (1079-1109): CHC: Error trying to invoke SMT solver.
// Warning 6328: (325-355): CHC: Assertion violation happens here.
// Warning 6328: (578-608): CHC: Assertion violation happens here.
// Warning 6328: (578-608): CHC: Assertion violation might happen here.
// Warning 6328: (691-721): CHC: Assertion violation might happen here.
// Warning 6328: (959-989): CHC: Assertion violation might happen here.
// Warning 6328: (1079-1109): CHC: Assertion violation might happen here.
// Warning 4661: (578-608): BMC: Assertion violation happens here.
// Warning 4661: (691-721): BMC: Assertion violation happens here.
// Warning 4661: (959-989): BMC: Assertion violation happens here.
// Warning 4661: (1079-1109): BMC: Assertion violation happens here.

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

@ -25,14 +25,16 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (579-609): CHC: Error trying to invoke SMT solver.
// Warning 1218: (692-722): CHC: Error trying to invoke SMT solver.
// Warning 1218: (960-990): CHC: Error trying to invoke SMT solver.
// Warning 1218: (1080-1110): CHC: Error trying to invoke SMT solver.
// Warning 6328: (326-356): CHC: Assertion violation happens here.
// Warning 6328: (579-609): CHC: Assertion violation happens here.
// Warning 6328: (579-609): CHC: Assertion violation might happen here.
// Warning 6328: (692-722): CHC: Assertion violation might happen here.
// Warning 6328: (960-990): CHC: Assertion violation might happen here.
// Warning 6328: (1080-1110): CHC: Assertion violation might happen here.
// Warning 4661: (579-609): BMC: Assertion violation happens here.
// Warning 4661: (692-722): BMC: Assertion violation happens here.
// Warning 4661: (960-990): BMC: Assertion violation happens here.
// Warning 4661: (1080-1110): BMC: Assertion violation happens here.

8
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_simple.sol
View File

@ -25,7 +25,9 @@ contract C {
// SMTEngine: all
// ----
// Warning 5667: (100-115): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 6328: (571-601): CHC: Assertion violation happens here.
// Warning 1218: (855-885): CHC: Error trying to invoke SMT solver.
// Warning 6328: (571-601): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0\nt = false\nx = 0\ny = 0\nz = 0\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeSimple(0, false, 0, 0, 0, a, b)
// Warning 6328: (691-721): CHC: Assertion violation happens here.
// Warning 6328: (740-770): CHC: Assertion violation happens here.
// Warning 6328: (855-885): CHC: Assertion violation happens here.
// Warning 6328: (740-770): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0\nt = false\nx = 0\ny = 0\nz = 0\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeSimple(0, false, 0, 0, 0, a, b)
// Warning 6328: (855-885): CHC: Assertion violation might happen here.
// Warning 4661: (855-885): BMC: Assertion violation happens here.

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

@ -22,15 +22,17 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (252-282): CHC: Error trying to invoke SMT solver.
// Warning 1218: (347-377): CHC: Error trying to invoke SMT solver.
// Warning 1218: (531-561): CHC: Error trying to invoke SMT solver.
// Warning 1218: (627-657): CHC: Error trying to invoke SMT solver.
// Warning 1218: (746-776): CHC: Error trying to invoke SMT solver.
// Warning 6328: (252-282): CHC: Assertion violation happens here.
// Warning 6328: (252-282): CHC: Assertion violation might happen here.
// Warning 6328: (347-377): CHC: Assertion violation might happen here.
// Warning 6328: (531-561): CHC: Assertion violation might happen here.
// Warning 6328: (627-657): CHC: Assertion violation might happen here.
// Warning 6328: (746-776): CHC: Assertion violation might happen here.
// Warning 4661: (252-282): BMC: Assertion violation happens here.
// Warning 4661: (347-377): BMC: Assertion violation happens here.
// Warning 4661: (531-561): BMC: Assertion violation happens here.
// Warning 4661: (627-657): BMC: Assertion violation happens here.

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

@ -25,14 +25,16 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (588-618): CHC: Error trying to invoke SMT solver.
// Warning 1218: (702-732): CHC: Error trying to invoke SMT solver.
// Warning 1218: (971-1001): CHC: Error trying to invoke SMT solver.
// Warning 1218: (1086-1116): CHC: Error trying to invoke SMT solver.
// Warning 6328: (334-364): CHC: Assertion violation happens here.
// Warning 6328: (588-618): CHC: Assertion violation happens here.
// Warning 6328: (588-618): CHC: Assertion violation might happen here.
// Warning 6328: (702-732): CHC: Assertion violation might happen here.
// Warning 6328: (971-1001): CHC: Assertion violation might happen here.
// Warning 6328: (1086-1116): CHC: Assertion violation might happen here.
// Warning 4661: (588-618): BMC: Assertion violation happens here.
// Warning 4661: (702-732): BMC: Assertion violation happens here.
// Warning 4661: (971-1001): BMC: Assertion violation happens here.
// Warning 4661: (1086-1116): BMC: Assertion violation happens here.

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

@ -25,14 +25,16 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (589-619): CHC: Error trying to invoke SMT solver.
// Warning 1218: (703-733): CHC: Error trying to invoke SMT solver.
// Warning 1218: (972-1002): CHC: Error trying to invoke SMT solver.
// Warning 1218: (1087-1117): CHC: Error trying to invoke SMT solver.
// Warning 6328: (335-365): CHC: Assertion violation happens here.
// Warning 6328: (589-619): CHC: Assertion violation happens here.
// Warning 6328: (589-619): CHC: Assertion violation might happen here.
// Warning 6328: (703-733): CHC: Assertion violation might happen here.
// Warning 6328: (972-1002): CHC: Assertion violation might happen here.
// Warning 6328: (1087-1117): CHC: Assertion violation might happen here.
// Warning 4661: (589-619): BMC: Assertion violation happens here.
// Warning 4661: (703-733): BMC: Assertion violation happens here.
// Warning 4661: (972-1002): BMC: Assertion violation happens here.
// Warning 4661: (1087-1117): BMC: Assertion violation happens here.

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

@ -24,7 +24,9 @@ contract C {
// SMTEngine: all
// ----
// Warning 5667: (107-122): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 1218: (824-854): CHC: Error trying to invoke SMT solver.
// Warning 6328: (543-573): CHC: Assertion violation happens here.
// Warning 6328: (664-694): CHC: Assertion violation happens here.
// Warning 6328: (713-743): CHC: Assertion violation happens here.
// Warning 6328: (824-854): CHC: Assertion violation happens here.
// Warning 6328: (824-854): CHC: Assertion violation might happen here.
// Warning 4661: (824-854): BMC: Assertion violation happens here.

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

@ -22,15 +22,17 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (261-291): CHC: Error trying to invoke SMT solver.
// Warning 1218: (357-387): CHC: Error trying to invoke SMT solver.
// Warning 1218: (542-572): CHC: Error trying to invoke SMT solver.
// Warning 1218: (639-669): CHC: Error trying to invoke SMT solver.
// Warning 1218: (753-783): CHC: Error trying to invoke SMT solver.
// Warning 6328: (261-291): CHC: Assertion violation happens here.
// Warning 6328: (261-291): CHC: Assertion violation might happen here.
// Warning 6328: (357-387): CHC: Assertion violation might happen here.
// Warning 6328: (542-572): CHC: Assertion violation might happen here.
// Warning 6328: (639-669): CHC: Assertion violation might happen here.
// Warning 6328: (753-783): CHC: Assertion violation might happen here.
// Warning 4661: (261-291): BMC: Assertion violation happens here.
// Warning 4661: (357-387): BMC: Assertion violation happens here.
// Warning 4661: (542-572): BMC: Assertion violation happens here.
// Warning 4661: (639-669): BMC: Assertion violation happens here.

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

@ -14,5 +14,5 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (139-161): CHC: Assertion violation happens here.\nCounterexample:\ndata = [98]\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.g()
// Warning 6328: (139-161): CHC: Assertion violation happens here.
// Warning 6328: (263-290): CHC: Assertion violation happens here.\nCounterexample:\ndata = [1]\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.g()

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

@ -21,4 +21,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (362-420): CHC: Assertion violation happens here.\nCounterexample:\nc = [[2]]\n\nTransaction trace:\nC.constructor()\nState: c = []\nC.g()
// Warning 6328: (362-420): CHC: Assertion violation happens here.

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

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

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

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

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

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

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

@ -23,4 +23,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (435-508): CHC: Assertion violation happens here.\nCounterexample:\nc = [[2]]\nval = 2\n\nTransaction trace:\nC.constructor()\nState: c = []\nC.g()
// Warning 6328: (435-508): CHC: Assertion violation happens here.

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

@ -12,5 +12,5 @@ contract C {
// SMTEngine: all
// ----
// 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.\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()
// Warning 6328: (170-186): CHC: Assertion violation happens here.
// Warning 6328: (190-246): CHC: Assertion violation happens here.

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

@ -14,5 +14,5 @@ contract C {
// 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-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 6368: (188-195): CHC: Out of bounds access 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()

3
test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol
View File

@ -1,4 +1,5 @@
contract C {
constructor() payable {}
function f(address payable a) public {
require(address(this).balance > 1000);
a.transfer(666);
@ -11,4 +12,4 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (166-201): CHC: Assertion violation happens here.
// Warning 6328: (192-227): CHC: Assertion violation happens here.

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

@ -33,4 +33,6 @@ contract C {
// Warning 2072: (435-445): Unused local variable.
// Warning 2072: (656-666): Unused local variable.
// Warning 2072: (698-708): Unused local variable.
// Warning 6328: (135-151): CHC: Assertion violation happens here.
// Warning 1218: (135-151): CHC: Error trying to invoke SMT solver.
// Warning 6328: (135-151): CHC: Assertion violation might happen here.
// Warning 4661: (135-151): BMC: Assertion violation happens here.

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

@ -14,4 +14,4 @@ contract C {
// Warning 2519: (100-106): This declaration shadows an existing declaration.
// Warning 2072: (100-106): Unused local variable.
// Warning 2072: (108-125): Unused local variable.
// Warning 6328: (143-157): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\ns = false\ndata = [36, 5, 5, 5, 5, 5]\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.s(1)\nState: x = 1\nC.f(0)\n a.call("") -- untrusted external call
// Warning 6328: (143-157): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\ns = false\ndata = [9, 9, 44, 9, 9, 30, 9, 9, 9, 9]\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.s(1)\nState: x = 1\nC.f(0)\n a.call("") -- untrusted external call

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

@ -20,4 +20,4 @@ contract C {
// 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: (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/external_calls/external_hash_known_code_state_reentrancy_2.sol
View File

@ -40,4 +40,4 @@ contract C {
// SMTEngine: all
// ----
// Warning 2018: (33-88): Function state mutability can be restricted to view
// Warning 6328: (367-381): CHC: Assertion violation happens here.\nCounterexample:\nowner = 0, y = 0, z = 3, s = 0, insidef = true\nprevOwner = 0\n\nTransaction trace:\nC.constructor()\nState: owner = 0, y = 0, z = 0, s = 0, insidef = false\nC.f()\n s.f() -- untrusted external call, synthesized as:\n C.zz() -- reentrant call
// Warning 6328: (367-381): CHC: Assertion violation happens here.

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

@ -35,5 +35,7 @@ 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 happens here.
// Warning 6328: (366-392): CHC: Assertion violation might happen here.
// Warning 4661: (366-392): BMC: Assertion violation happens here.

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

@ -27,5 +27,6 @@ contract C is A {
// ====
// SMTEngine: all
// ----
// Warning 1218: (352-366): CHC: Error trying to invoke SMT solver.
// Warning 6328: (154-168): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.f()
// Warning 6328: (352-366): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\nd = 0\n\nTransaction trace:\nC.constructor()\nState: x = 1\nC.call(0)\n d.d() -- untrusted external call, synthesized as:\n C.f() -- reentrant call
// Warning 6328: (352-366): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 1\nC.f()

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

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

4
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 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: (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: (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 = 8\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.

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

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

2
test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_1.sol
View File

@ -15,4 +15,4 @@ contract C is B {
// ====
// SMTEngine: all
// ----
// Warning 6328: (52-66): CHC: Assertion violation happens here.
// Warning 6328: (52-66): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 1\n\nTransaction trace:\nC.constructor()\nState: y = 0, x = 0\nC.g()\n B.f() -- internal call\nState: y = 0, x = 1\nB.f()

2
test/libsolidity/smtCheckerTests/inheritance/receive_fallback.sol
View File

@ -21,6 +21,6 @@ contract B is A {
// ====
// SMTEngine: all
// ----
// Warning 6328: (87-101): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.receive(){ value: 10450 }
// Warning 6328: (87-101): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.receive(){ value: 2 }
// Warning 6328: (136-150): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.g()
// Warning 6328: (255-269): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 0\n\nTransaction trace:\nB.constructor()\nState: y = 0, x = 0\nB.fallback()

3
test/libsolidity/smtCheckerTests/invariants/aon_blog_post.sol
View File

@ -45,4 +45,5 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (657-667): CHC: Assertion violation happens here.
// Warning 6328: (657-667): CHC: Assertion violation might happen here.
// Warning 4661: (657-667): BMC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol
View File

@ -23,6 +23,7 @@ contract LoopFor2 {
// SMTIgnoreCex: yes
// ----
// Warning 2072: (202-217): Unused local variable.
// Warning 1218: (371-375): CHC: Error trying to invoke SMT solver.
// Warning 6368: (354-358): CHC: Out of bounds access happens here.
// Warning 6368: (371-375): CHC: Out of bounds access happens here.
// Warning 6368: (371-375): CHC: Out of bounds access might happen here.
// Warning 6368: (378-382): CHC: Out of bounds access happens here.

4
test/libsolidity/smtCheckerTests/loops/while_nested_continue_fail.sol
View File

@ -27,5 +27,7 @@ contract C
// ====
// SMTEngine: all
// ----
// Warning 6328: (290-305): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 15\nb = false\nc = false\n\nTransaction trace:\nC.constructor()\nC.f(0, 0, false, false)
// Warning 1218: (290-305): CHC: Error trying to invoke SMT solver.
// Warning 6328: (290-305): CHC: Assertion violation might happen here.
// Warning 6328: (329-344): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 15\ny = 0\nb = true\nc = false\n\nTransaction trace:\nC.constructor()\nC.f(0, 0, true, false)
// Warning 4661: (290-305): BMC: Assertion violation happens 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: (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 = 1\nz = 0\nt = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(1)\n C.f1(1) -- internal call
// 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

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 = [0, 200]\nx = 0\np = 1\n\nTransaction trace:\nC.constructor()\nState: array = [0, 0]\nC.f(0, 1)
// 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)

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

@ -12,4 +12,4 @@ contract C
// ====
// SMTEngine: all
// ----
// Warning 6328: (165-185): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\np = 38\n\nTransaction trace:\nC.constructor()\nC.f(0, 38)
// Warning 6328: (165-185): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\np = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, 0)

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

@ -12,4 +12,4 @@ contract C
// ====
// SMTEngine: all
// ----
// Warning 6328: (164-183): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\np = 38\n\nTransaction trace:\nC.constructor()\nC.f(0, 38)
// Warning 6328: (164-183): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\np = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, 0)

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

@ -17,4 +17,4 @@ contract C {
// SMTEngine: all
// ----
// Warning 6328: (143-190): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[]]\nlength = 0\nlength2 = 0\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.s()
// Warning 6328: (363-408): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[], [0]]\nlength = 2\nlength2 = 1\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.s()
// Warning 6328: (363-408): CHC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/operators/index_access_for_bytesNN.sol
View File

@ -7,3 +7,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6368: (76-90): CHC: Out of bounds access might happen here.

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

@ -13,4 +13,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 4984: (61-64): CHC: Overflow (resulting value larger than 255) happens here.
// Warning 4984: (61-64): CHC: Overflow (resulting value larger than 255) happens here.\nCounterexample:\nx = 255\n\nTransaction trace:\nC.constructor()\nState: x = 254\nC.inc_pre()\nState: x = 255\nC.inc_pre()

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

@ -21,4 +21,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 4984: (112-117): CHC: Overflow (resulting value larger than 255) happens here.
// Warning 4984: (112-117): CHC: Overflow (resulting value larger than 255) happens here.\nCounterexample:\ns = {x: 255}\n\nTransaction trace:\nC.constructor()\nState: s = {x: 254}\nC.inc_pre()\nState: s = {x: 255}\nC.inc_pre()

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

@ -20,7 +20,5 @@ contract C {
// SMTEngine: all
// ----
// 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.
// 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()
// 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.

11
test/libsolidity/smtCheckerTests/out_of_bounds/array_2d_4.sol
View File

@ -14,10 +14,15 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 1218: (228-232): CHC: Error trying to invoke SMT solver.
// Warning 1218: (255-259): CHC: Error trying to invoke SMT solver.
// Warning 1218: (255-262): CHC: Error trying to invoke SMT solver.
// Warning 4984: (184-197): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6368: (228-232): CHC: Out of bounds access happens here.\nCounterexample:\na = []\ni = 0\nj = 0\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.r()
// Warning 4984: (199-202): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6368: (228-232): CHC: Out of bounds access might happen here.
// Warning 4984: (228-244): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6368: (255-259): CHC: Out of bounds access happens here.\nCounterexample:\na = []\ni = 0\nj = 0\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.r()
// Warning 6368: (255-262): CHC: Out of bounds access happens here.\nCounterexample:\na = []\ni = 0\nj = 0\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.r()
// Warning 4984: (246-249): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6368: (255-259): CHC: Out of bounds access might happen here.
// Warning 6368: (255-262): CHC: Out of bounds access might happen here.
// Warning 2661: (184-197): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 2661: (228-244): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

5
test/libsolidity/smtCheckerTests/out_of_bounds/fixed_bytes_4.sol
View File

@ -1,10 +1,11 @@
contract C {
function r(bytes32 x, uint y) public pure {
x[0]; // safe access
x[y]; // oob access
// Disabled because of Spacer nondeterminism.
//x[y]; // oob access
}
}
// ====
// SMTEngine: all
// ----
// Warning 6368: (83-87): CHC: Out of bounds access happens here.
// Warning 5667: (36-42): Unused function parameter. Remove or comment out the variable name to silence this warning.

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

@ -7,4 +7,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 4984: (96-101): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = 57896044618658097711785492504343953926634992332820282019728792003956564819967\ny = (- 1)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(57896044618658097711785492504343953926634992332820282019728792003956564819967, (- 1))
// Warning 4984: (96-101): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = 0\ny = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, (- 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 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 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 6328: (220-236): CHC: Assertion violation happens here.\nCounterexample:\n\na1 = 2437\nb1 = 10\nc1 = 9\na2 = 2437\nb2 = 10\nc2 = 9\n\nTransaction trace:\nC.constructor()\nC.f(data)
// 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)

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: (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
// 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

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

@ -13,4 +13,4 @@ contract B {
// ====
// SMTEngine: all
// ----
// Warning 6328: (154-176): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nB.constructor(){ value: 1 }
// Warning 6328: (154-176): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nB.constructor(){ value: 39 }

4
test/libsolidity/smtCheckerTests/try_catch/try_4.sol
View File

@ -25,5 +25,7 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (178-192): CHC: Assertion violation happens here.
// Warning 1218: (178-192): CHC: Error trying to invoke SMT solver.
// Warning 6328: (178-192): CHC: Assertion violation might happen here.
// Warning 6328: (318-332): CHC: Assertion violation happens here.
// Warning 4661: (178-192): BMC: Assertion violation happens here.

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

@ -20,4 +20,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6328: (323-343): CHC: Assertion violation happens here.\nCounterexample:\n\nchoice = 3\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (323-343): CHC: Assertion violation happens here.\nCounterexample:\n\nchoice = 1\n\nTransaction trace:\nC.constructor()\nC.f()\n C.g() -- trusted external call

4
test/libsolidity/smtCheckerTests/types/address_balance.sol
View File

@ -9,5 +9,5 @@ contract C
// SMTEngine: all
// ----
// Warning 2072: (63-69): Unused local variable.
// Warning 4984: (72-94): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\na = 0\nb = 38\nx = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, 38)
// Warning 6328: (98-127): CHC: Assertion violation happens here.\nCounterexample:\n\na = 21238\nb = 7719\nx = 1000000000000000000038\n\nTransaction trace:\nC.constructor()\nC.f(21238, 7719)
// Warning 4984: (72-94): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\na = 0\nb = 0\nx = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, 0)
// Warning 6328: (98-127): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\nb = 0\nx = 1000000000000000008931\n\nTransaction trace:\nC.constructor()\nC.f(0, 0)

5
test/libsolidity/smtCheckerTests/types/address_transfer.sol
View File

@ -1,5 +1,6 @@
contract C
{
constructor() payable {}
function f(address payable a) public {
uint x = 100;
require(x == a.balance);
@ -11,5 +12,5 @@ contract C
// ====
// SMTEngine: all
// ----
// Warning 6328: (162-186): CHC: Assertion violation happens here.\nCounterexample:\n\na = 38\nx = 100\n\nTransaction trace:\nC.constructor()\nC.f(38)
// Warning 1236: (98-113): BMC: Insufficient funds happens here.
// Warning 6328: (188-212): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\nx = 100\n\nTransaction trace:\nC.constructor(){ value: 57 }\nC.f(0)
// Warning 1236: (124-139): BMC: Insufficient funds happens here.

7
test/libsolidity/smtCheckerTests/types/address_transfer_2.sol
View File

@ -1,5 +1,6 @@
contract C
{
constructor() payable {}
function f(uint x, address payable a, address payable b) public {
require(a != b);
require(x == 100);
@ -15,6 +16,6 @@ contract C
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (262-291): CHC: Assertion violation happens here.
// Warning 1236: (184-199): BMC: Insufficient funds happens here.
// Warning 1236: (203-218): BMC: Insufficient funds happens here.
// Warning 6328: (288-317): CHC: Assertion violation happens here.
// Warning 1236: (210-225): BMC: Insufficient funds happens here.
// Warning 1236: (229-244): BMC: Insufficient funds happens here.

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

@ -11,6 +11,6 @@ contract C
// ====
// SMTEngine: all
// ----
// Warning 6328: (180-204): CHC: Assertion violation happens here.\nCounterexample:\n\na = 7719\nb = 7719\n\nTransaction trace:\nC.constructor()\nC.f(7719, 7719)
// Warning 6328: (180-204): CHC: Assertion violation happens here.\nCounterexample:\n\na = 8855\nb = 8855\n\nTransaction trace:\nC.constructor()\nC.f(8855, 8855)
// Warning 1236: (101-116): BMC: Insufficient funds happens here.
// Warning 1236: (120-136): BMC: Insufficient funds happens here.

11
test/libsolidity/smtCheckerTests/types/array_aliasing_storage_3.sol
View File

@ -35,7 +35,12 @@ contract C
// SMTIgnoreCex: yes
// ----
// Warning 2072: (384-399): Unused local variable.
// Warning 1218: (955-959): CHC: Error trying to invoke SMT solver.
// Warning 1218: (948-965): CHC: Error trying to invoke SMT solver.
// Warning 1218: (976-980): CHC: Error trying to invoke SMT solver.
// Warning 6368: (489-493): CHC: Out of bounds access happens here.
// Warning 6368: (955-959): CHC: Out of bounds access happens here.
// Warning 6328: (948-965): CHC: Assertion violation happens here.
// Warning 6368: (976-980): CHC: Out of bounds access happens here.
// Warning 6368: (955-959): CHC: Out of bounds access might happen here.
// Warning 6328: (948-965): CHC: Assertion violation might happen here.
// Warning 6368: (976-980): CHC: Out of bounds access might happen here.
// Warning 4661: (948-965): BMC: Assertion violation happens here.
// Warning 4661: (948-965): BMC: Assertion violation happens here.

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

@ -33,11 +33,18 @@ contract C
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 1218: (367-371): CHC: Error trying to invoke SMT solver.
// Warning 1218: (490-494): CHC: Error trying to invoke SMT solver.
// Warning 1218: (692-696): CHC: Error trying to invoke SMT solver.
// Warning 1218: (685-702): CHC: Error trying to invoke SMT solver.
// Warning 1218: (796-800): CHC: Error trying to invoke SMT solver.
// Warning 6368: (329-333): 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: (367-371): CHC: Out of bounds access happens here.
// Warning 6368: (490-494): CHC: Out of bounds access happens here.
// Warning 6368: (692-696): CHC: Out of bounds access happens here.
// Warning 6328: (685-702): CHC: Assertion violation happens here.
// Warning 6368: (796-800): CHC: Out of bounds access happens here.
// Warning 6368: (367-371): CHC: Out of bounds access might happen here.
// Warning 6368: (490-494): CHC: Out of bounds access might happen here.
// Warning 6368: (692-696): CHC: Out of bounds access might happen here.
// Warning 6328: (685-702): CHC: Assertion violation might happen here.
// Warning 6368: (796-800): CHC: Out of bounds access might happen here.
// Warning 4661: (685-702): BMC: Assertion violation happens here.
// Warning 4661: (685-702): BMC: Assertion violation happens here.

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

@ -11,4 +11,4 @@ contract C
// SMTEngine: all
// ----
// Warning 6368: (98-106): CHC: Out of bounds access happens here.\nCounterexample:\narray = []\nx = 0\ny = 0\nz = 0\nt = 0\n\nTransaction trace:\nC.constructor()\nState: array = []\nC.f(0, 0, 0, 0)
// Warning 6368: (98-109): CHC: Out of bounds access happens here.\nCounterexample:\narray = []\nx = 38\ny = 0\nz = 0\nt = 0\n\nTransaction trace:\nC.constructor()\nState: array = []\nC.f(38, 0, 0, 0)
// Warning 6368: (98-109): CHC: Out of bounds access happens here.\nCounterexample:\narray = []\nx = 0\ny = 0\nz = 0\nt = 0\n\nTransaction trace:\nC.constructor()\nState: array = []\nC.f(0, 0, 0, 0)

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

@ -11,4 +11,4 @@ contract C
// ====
// SMTEngine: all
// ----
// Warning 6328: (135-157): CHC: Assertion violation happens here.\nCounterexample:\narray = [0, 0, 0, 0, 0, 0, 0, 0, 0, 200]\nx = 9\ny = 9\n\nTransaction trace:\nC.constructor()\nState: array = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0]\nC.f(9, 9)
// Warning 6328: (135-157): CHC: Assertion violation happens here.\nCounterexample:\narray = [200, 0, 0, 0, 0, 0, 0, 0, 0, 0]\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: array = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0]\nC.f(0, 0)

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

@ -12,4 +12,4 @@ contract C
// ====
// SMTEngine: all
// ----
// Warning 6328: (214-239): CHC: Assertion violation happens here.\nCounterexample:\narray = [[0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0]]\nx = 19\ny = 8\nz = 19\nt = 8\n\nTransaction trace:\nC.constructor()\nState: array = [[0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0]]\nC.f(19, 8, 19, 8)
// Warning 6328: (214-239): CHC: Assertion violation happens here.\nCounterexample:\narray = [[0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0]]\nx = 0\ny = 0\nz = 0\nt = 0\n\nTransaction trace:\nC.constructor()\nState: array = [[0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0]]\nC.f(0, 0, 0, 0)

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

File diff suppressed because one or more lines are too long

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

@ -8,4 +8,4 @@ contract C
// ====
// SMTEngine: all
// ----
// Warning 6328: (92-111): CHC: Assertion violation happens here.\nCounterexample:\n\na = 38\nx = 0\n\nTransaction trace:\nC.constructor()\nC.f(38, 0)
// Warning 6328: (92-111): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\nx = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, 0)

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

@ -16,5 +16,5 @@ contract c {
// ====
// SMTEngine: all
// ----
// Warning 6328: (255-291): CHC: Assertion violation happens here.\nCounterexample:\n\ncond = true\n\nTransaction trace:\nc.constructor()\nc.f(true)
// Warning 6328: (255-291): CHC: Assertion violation happens here.
// Warning 6328: (303-339): CHC: Assertion violation happens here.\nCounterexample:\n\ncond = false\n\nTransaction trace:\nc.constructor()\nc.f(false)