From 839bc6f698bab436006cbf38ac7fd2697281e693 Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Thu, 15 Jul 2021 12:49:58 +0200 Subject: [PATCH] Enable tests that were killed by oom or seg fault --- .../push_storage_ref_unsafe_length.sol | 5 +- .../blockchain_state/decreasing_balance.sol | 4 +- .../unary_add_minus_overflow_detected.sol | 4 +- .../external_calls/external_inc1_inc2.sol | 7 +- .../getters/nested_arrays_mappings_3.sol | 4 +- .../getters/nested_arrays_mappings_6.sol | 4 +- .../invariants/state_machine_1_fail.sol | 4 +- ...or_loop_array_assignment_memory_memory.sol | 17 +- ...r_loop_array_assignment_memory_storage.sol | 23 +- ...le_loop_array_assignment_memory_memory.sol | 24 +- ...e_loop_array_assignment_memory_storage.sol | 19 +- .../unary_add_minus_overflow_detected.sol | 5 +- .../try_string_literal_to_bytes_array.sol | 4 +- .../types/array_aliasing_memory_2.sol | 9 +- .../types/array_aliasing_memory_3.sol | 8 +- .../types/array_aliasing_storage_1.sol | 11 +- .../types/array_aliasing_storage_3.sol | 15 +- .../types/array_aliasing_storage_5.sol | 11 +- .../types/array_mapping_aliasing_1.sol | 6 +- .../types/array_static_aliasing_memory_5.sol | 9 +- .../types/array_static_aliasing_storage_5.sol | 9 +- .../types/array_static_mapping_aliasing_1.sol | 6 +- .../types/mapping_aliasing_2.sol | 4 +- ...rray_struct_array_struct_memory_unsafe.sol | 22 +- .../types/struct/struct_aliasing_storage.sol | 9 +- ...uct_array_struct_array_memory_unsafe_2.sol | 22 +- .../types/struct/struct_mapping.sol | 4 +- .../types/struct/struct_recursive_3.sol | 280 +++++++++++------- .../types/struct_array_branches_3d.sol | 7 +- 29 files changed, 322 insertions(+), 234 deletions(-) diff --git a/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol index ea55e3055..730ccdf6c 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol @@ -19,8 +19,7 @@ contract C { // Access is safe but oob reported due to aliasing. assert(c[0][0][0] == 12); // Safe but knowledge about `d` is erased because `b` could be pointing to `d`. - // Removed assertion because current Spacer seg faults in cex generation. - //assert(d[1] == 7); + assert(d[1] == 7); } } // ==== @@ -36,3 +35,5 @@ contract C { // Warning 6368: (513-520): CHC: Out of bounds access happens here. // Warning 6368: (513-523): CHC: Out of bounds access happens here. // Warning 6328: (506-530): CHC: Assertion violation happens here. +// Warning 6368: (623-627): CHC: Out of bounds access happens here. +// Warning 6328: (616-633): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol b/test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol index 7bbbf9ddb..6ff141efe 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol @@ -11,10 +11,10 @@ contract C { // If only looking at `f`, it looks like this.balance always decreases. // However, the edge case of a contract `selfdestruct` sending its remaining balance // to this contract should make the claim false (since there's no fallback/receive here). - // Removed because current Spacer seg faults in cex generation. - //assert(address(this).balance == t); + assert(address(this).balance == t); } } // ==== // SMTEngine: all // ---- +// Warning 6328: (463-497): CHC: Assertion violation happens here.\nCounterexample:\nt = 2211\n\nTransaction trace:\nC.constructor()\nState: t = 2211\nC.f(2112, 1)\nState: t = 2211\nC.inv() diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/unary_add_minus_overflow_detected.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/unary_add_minus_overflow_detected.sol index 085be4618..ccb7da1a0 100644 --- a/test/libsolidity/smtCheckerTests/bmc_coverage/unary_add_minus_overflow_detected.sol +++ b/test/libsolidity/smtCheckerTests/bmc_coverage/unary_add_minus_overflow_detected.sol @@ -9,7 +9,6 @@ contract C { --x; } - /* Commented out because Spacer segfaults in Z3 4.8.9 function inc_post() public { x++; } @@ -17,7 +16,6 @@ contract C { function dec_post() public { x--; } - */ } // ==== @@ -25,3 +23,5 @@ contract C { // ---- // Warning 2661: (55-58): BMC: Overflow (resulting value larger than 255) happens here. // Warning 4144: (95-98): BMC: Underflow (resulting value less than 0) happens here. +// Warning 2661: (139-142): BMC: Overflow (resulting value larger than 255) happens here. +// Warning 4144: (180-183): BMC: Underflow (resulting value less than 0) happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_inc1_inc2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_inc1_inc2.sol index 25a93b233..317f5da71 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_inc1_inc2.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_inc1_inc2.sol @@ -18,12 +18,11 @@ contract C { function f() public { uint oldX = x; - // Removed because Spacer 4.8.9 seg faults. - //d.d(); - assert(oldX == x); + d.d(); + assert(oldX == x); // should fail } } // ==== // SMTEngine: all // ---- -// Warning 2018: (203-322): Function state mutability can be restricted to view +// Warning 6328: (253-270): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_3.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_3.sol index 97cc03919..35ae018b7 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_3.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_3.sol @@ -17,10 +17,10 @@ contract C { function f() public view { uint y = this.m(0,1,2,3); assert(y == m[0][1][2][3]); // should hold - // Disabled because of Spacer seg fault - //assert(y == 1); // should fail + assert(y == 1); // should fail } } // ==== // SMTEngine: all // ---- +// Warning 6328: (368-382): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_6.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_6.sol index 3ad4d94ae..3bb702fdd 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_6.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_6.sol @@ -12,10 +12,10 @@ contract C { function f() public view { uint y = this.m(0,1,2,3); assert(y == m[0][1][2][3]); // should hold - // Disabled because Spacer seg faults - //assert(y == 1); // should fail + assert(y == 1); // should fail } } // ==== // SMTEngine: all // ---- +// Warning 6328: (316-330): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/invariants/state_machine_1_fail.sol b/test/libsolidity/smtCheckerTests/invariants/state_machine_1_fail.sol index b8727aab4..a8c2dc65d 100644 --- a/test/libsolidity/smtCheckerTests/invariants/state_machine_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/invariants/state_machine_1_fail.sol @@ -23,11 +23,11 @@ contract C { // Fails due to j. function i() public view { - // Disabled because Spacer 4.8.9 seg faults. - //assert(x < 2); + assert(x < 2); // should fail } } // ==== // SMTEngine: all // SMTSolvers: z3 // ---- +// Warning 6328: (278-291): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol index 88fe7f51f..2b5b9d341 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol @@ -10,19 +10,22 @@ contract LoopFor2 { b[i] = i + 1; c[i] = b[i]; } - // Removed because current Spacer seg faults in cex generation. - //assert(b[0] == c[0]); - // Removed because current Spacer seg faults in cex generation. - //assert(a[0] == 900); - // Removed because current Spacer seg faults in cex generation. - //assert(b[0] == 900); + assert(b[0] == c[0]); // should fail due to aliasing + assert(a[0] == 900); // should fail due to aliasing + assert(b[0] == 900); // should fail due to aliasing } } // ==== // SMTEngine: all // SMTIgnoreCex: yes // ---- -// Warning 2072: (202-217): Unused local variable. // Warning 6368: (354-358): CHC: Out of bounds access happens here. // Warning 6368: (378-382): CHC: Out of bounds access happens here. // Warning 6368: (371-375): CHC: Out of bounds access happens here. +// Warning 6368: (397-401): CHC: Out of bounds access happens here. +// Warning 6368: (405-409): CHC: Out of bounds access happens here. +// Warning 6328: (390-410): CHC: Assertion violation happens here. +// Warning 6368: (452-456): CHC: Out of bounds access happens here. +// Warning 6328: (445-464): CHC: Assertion violation happens here. +// Warning 6368: (506-510): CHC: Out of bounds access happens here. +// Warning 6328: (499-518): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_storage.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_storage.sol index 359f82838..5d831dead 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_storage.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_storage.sol @@ -13,16 +13,27 @@ contract LoopFor2 { for (uint i = 0; i < n; i += 1) { // Accesses are safe but oob is reported due to potential aliasing after c's assignment. b[i] = i + 1; - // Disabled because of Spacer's nondeterminism. - //c[i] = b[i]; + c[i] = b[i]; } - // Removed because current Spacer seg faults in cex generation. - //assert(b[0] == c[0]); - //assert(a[0] == 900); - //assert(b[0] == 900); + assert(b[0] == c[0]); // should fail due to aliasing + assert(a[0] == 900); // should hold + assert(b[0] == 900); // should fail } } // ==== // SMTEngine: all // SMTSolvers: z3 // ---- +// Warning 6368: (409-413): CHC: Out of bounds access happens here. +// Warning 6368: (433-437): CHC: Out of bounds access happens here. +// Warning 1218: (426-430): CHC: Error trying to invoke SMT solver. +// Warning 6368: (426-430): CHC: Out of bounds access might happen here. +// Warning 1218: (452-456): CHC: Error trying to invoke SMT solver. +// Warning 6368: (452-456): CHC: Out of bounds access might happen here. +// Warning 1218: (460-464): CHC: Error trying to invoke SMT solver. +// Warning 6368: (460-464): CHC: Out of bounds access might happen here. +// Warning 6328: (445-465): CHC: Assertion violation happens here. +// Warning 6368: (545-549): CHC: Out of bounds access happens here. +// Warning 1218: (538-557): CHC: Error trying to invoke SMT solver. +// Warning 6328: (538-557): CHC: Assertion violation might happen here. +// Warning 4661: (538-557): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol index 6ee19dfa4..4f44bcd6f 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol @@ -6,21 +6,15 @@ contract LoopFor2 { b[0] = 900; uint[] memory a = b; uint i; - // Disabled because of Spacer's nondeterminism. - /* while (i < n) { // Accesses are safe but oob is reported due to potential aliasing after c's assignment. b[i] = i + 1; c[i] = b[i]; ++i; } - */ - // Removed because current Spacer seg faults in cex generation. - //assert(b[0] == c[0]); - // Removed because current Spacer seg faults in cex generation. - //assert(a[0] == 900); - // Removed because current Spacer seg faults in cex generation. - //assert(b[0] == 900); + assert(b[0] == c[0]); // should fail due to aliasing + assert(a[0] == 900); // should fail due to aliasing + assert(b[0] == 900); // should fail due to aliasing } } // ==== @@ -28,5 +22,13 @@ contract LoopFor2 { // SMTIgnoreCex: yes // SMTSolvers: z3 // ---- -// Warning 2072: (202-217): Unused local variable. -// Warning 2072: (225-231): Unused local variable. +// Warning 6368: (346-350): CHC: Out of bounds access happens here. +// Warning 6368: (370-374): CHC: Out of bounds access happens here. +// Warning 6368: (363-367): CHC: Out of bounds access happens here. +// Warning 6368: (397-401): CHC: Out of bounds access happens here. +// Warning 6368: (405-409): CHC: Out of bounds access happens here. +// Warning 6328: (390-410): CHC: Assertion violation happens here. +// Warning 6368: (452-456): CHC: Out of bounds access happens here. +// Warning 6328: (445-464): CHC: Assertion violation happens here. +// Warning 6368: (506-510): CHC: Out of bounds access happens here. +// Warning 6328: (499-518): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol index 788c36e37..a23ee0666 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol @@ -11,26 +11,29 @@ contract LoopFor2 { a = b; require(n > 0 && n < 100); uint i; - // Disabled because of Spacer nondeterminism. - /* while (i < n) { // Accesses are safe but oob is reported due to potential aliasing after c's assignment. b[i] = i + 1; c[i] = b[i]; ++i; } - */ // Fails due to aliasing, since both b and c are // memory references of same type. - // Removed because current Spacer seg faults in cex generation. - //assert(b[0] == c[0]); + assert(b[0] == c[0]); assert(a[0] == 900); - // Removed because current Spacer seg faults in cex generation. - //assert(b[0] == 900); + assert(b[0] == 900); } } // ==== // SMTEngine: all // SMTSolvers: z3 // ---- -// Warning 2072: (280-286): Unused local variable. +// Warning 6368: (401-405): CHC: Out of bounds access happens here. +// Warning 6368: (425-429): CHC: Out of bounds access happens here. +// Warning 1218: (418-422): CHC: Error trying to invoke SMT solver. +// Warning 6368: (418-422): CHC: Out of bounds access might happen here. +// Warning 6368: (540-544): CHC: Out of bounds access happens here. +// Warning 6368: (548-552): CHC: Out of bounds access happens here. +// Warning 6328: (533-553): CHC: Assertion violation happens here. +// Warning 6368: (587-591): CHC: Out of bounds access happens here. +// Warning 6328: (580-599): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/unary_add_minus_overflow_detected.sol b/test/libsolidity/smtCheckerTests/operators/unary_add_minus_overflow_detected.sol index 3ab970900..ef4e6bab4 100644 --- a/test/libsolidity/smtCheckerTests/operators/unary_add_minus_overflow_detected.sol +++ b/test/libsolidity/smtCheckerTests/operators/unary_add_minus_overflow_detected.sol @@ -9,7 +9,6 @@ contract C { --x; } - /* Commented out because Spacer segfaults in Z3 4.8.9 function inc_post() public { x++; } @@ -17,11 +16,13 @@ contract C { function dec_post() public { x--; } - */ } // ==== // SMTEngine: all // ---- // Warning 4984: (55-58): CHC: Overflow (resulting value larger than 255) might happen here. // Warning 3944: (95-98): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.dec_pre() +// Warning 4984: (136-139): CHC: Overflow (resulting value larger than 255) might happen here. +// Warning 3944: (180-183): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.dec_post() // Warning 2661: (55-58): BMC: Overflow (resulting value larger than 255) happens here. +// Warning 2661: (136-139): BMC: Overflow (resulting value larger than 255) happens here. diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_bytes_array.sol b/test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_bytes_array.sol index c557b08a0..83c53621f 100644 --- a/test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_bytes_array.sol +++ b/test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_bytes_array.sol @@ -7,8 +7,7 @@ contract C { function f() public view { try this.g() returns (bytes memory b) { assert(b[0] == bytes1(uint8(255)) && b[1] == bytes1(uint8(255))); // should hold - // Disabled because of Spacer seg fault - //assert(b[0] == bytes1(uint8(0)) || b[1] == bytes1(uint8(0))); // should fail + assert(b[0] == bytes1(uint8(0)) || b[1] == bytes1(uint8(0))); // should fail } catch { } } @@ -16,3 +15,4 @@ contract C { // ==== // SMTEngine: all // ---- +// Warning 6328: (246-306): CHC: Assertion violation happens here.\nCounterexample:\n\nb = [255, 255]\n\nTransaction trace:\nC.constructor()\nC.f()\n C.g() -- trusted external call diff --git a/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_2.sol b/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_2.sol index 7eccaf68f..e638539ee 100644 --- a/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_2.sol +++ b/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_2.sol @@ -16,8 +16,7 @@ contract C b[0] = 1; // Erasing knowledge about memory references should not // erase knowledge about state variables. - // Removed because current Spacer seg faults. - //assert(array[0] == 42); + assert(array[0] == 42); // Accesses are safe but oob is reported due of aliasing. assert(a[0] == 2); assert(b[0] == 1); @@ -28,6 +27,6 @@ contract C // SMTIgnoreCex: yes // ---- // Warning 6368: (327-331): CHC: Out of bounds access happens here. -// Warning 6368: (584-588): CHC: Out of bounds access happens here. -// Warning 6328: (577-594): CHC: Assertion violation happens here. -// Warning 6368: (605-609): CHC: Out of bounds access happens here. +// Warning 6368: (534-538): CHC: Out of bounds access happens here. +// Warning 6328: (527-544): CHC: Assertion violation happens here. +// Warning 6368: (555-559): CHC: Out of bounds access happens here. diff --git a/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_3.sol b/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_3.sol index 36b851ff3..dccb8866b 100644 --- a/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_3.sol +++ b/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_3.sol @@ -19,12 +19,12 @@ contract C // Erasing knowledge about memory references should not // erase knowledge about storage references. assert(c[0] == 42); - // Removed because current Spacer seg faults in cex generation. - //assert(a[0] == 2); - // Removed because current Spacer seg faults in cex generation. - //assert(b[0] == 1); + assert(a[0] == 2); + assert(b[0] == 1); } } // ==== // SMTEngine: all // ---- +// Warning 6368: (537-541): CHC: Out of bounds access happens here. +// Warning 6328: (530-547): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_1.sol b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_1.sol index 3f1b6cdd4..3beba6f2d 100644 --- a/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_1.sol +++ b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_1.sol @@ -44,12 +44,17 @@ contract C require(c < array4d[c].length); require(d < tinyArray3d.length); require(e < array4d.length); - // Disabled because of Spacer seg fault. - //f(array2d[a], array2d[b], array4d[c][c], tinyArray3d[d], array4d[e]); + f(array2d[a], array2d[b], array4d[c][c], tinyArray3d[d], array4d[e]); } } // ==== // SMTEngine: all // SMTIgnoreCex: yes // ---- -// Warning 2018: (957-1329): Function state mutability can be restricted to view +// Warning 6368: (1124-1134): CHC: Out of bounds access might happen here. +// Warning 6368: (1214-1224): CHC: Out of bounds access might happen here. +// Warning 6368: (1226-1236): CHC: Out of bounds access might happen here. +// Warning 6368: (1238-1248): CHC: Out of bounds access might happen here. +// Warning 6368: (1238-1251): CHC: Out of bounds access might happen here. +// Warning 6368: (1253-1267): CHC: Out of bounds access might happen here. +// Warning 6368: (1269-1279): CHC: Out of bounds access might happen here. diff --git a/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_3.sol b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_3.sol index f74fad8af..975e8f4e0 100644 --- a/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_3.sol +++ b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_3.sol @@ -18,12 +18,10 @@ contract C b[0] = 1; // Erasing knowledge about storage references should not // erase knowledge about memory references. - // Disabled because of Spacer's seg fault. - //assert(c[0] == 42); + assert(c[0] == 42); // Erasing knowledge about storage references should not // erase knowledge about memory references. - // Disabled because of Spacer's seg fault. - //assert(d[0] == 42); + assert(d[0] == 42); // Fails because b == a is possible. // Accesses are safe but oob is reported due of aliasing. assert(a[0] == 2); @@ -34,8 +32,9 @@ contract C // SMTEngine: all // SMTIgnoreCex: yes // ---- -// Warning 2072: (384-399): Unused local variable. // 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: (740-744): CHC: Out of bounds access happens here. +// Warning 6328: (733-751): CHC: Assertion violation happens here. +// Warning 6368: (861-865): CHC: Out of bounds access happens here. +// Warning 6328: (854-871): CHC: Assertion violation happens here. +// Warning 6368: (882-886): CHC: Out of bounds access 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 9f111dfb4..64d739170 100644 --- a/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_5.sol +++ b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_5.sol @@ -20,8 +20,7 @@ contract C // erase knowledge about memory references. assert(c[0] == 42); // Fails because d == a is possible. - // Removed because current Spacer seg faults in cex generation. - //assert(d[0] == 42); + assert(d[0] == 42); // Fails because b == a and d == a are possible. assert(a[0] == 2); // b == a is possible, but does not fail because b @@ -38,6 +37,8 @@ contract C // 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: (551-555): CHC: Out of bounds access happens here. +// Warning 6328: (544-562): CHC: Assertion violation happens here. +// Warning 6368: (624-628): CHC: Out of bounds access happens here. +// Warning 6328: (617-634): CHC: Assertion violation happens here. +// Warning 6368: (728-732): CHC: Out of bounds access happens here. diff --git a/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_1.sol b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_1.sol index 65f629cb2..508a995f3 100644 --- a/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_1.sol +++ b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_1.sol @@ -24,8 +24,7 @@ contract C // Should not fail since knowledge is erased only for mapping (uint => uint). assert(severalMaps8[0][0] == 42); // Should fail since map == severalMaps3d[0][0] is possible. - // Removed because current Spacer seg faults in cex generation. - //assert(severalMaps3d[0][0][0] == 42); + assert(severalMaps3d[0][0][0] == 42); } function g(uint x) public { require(x < severalMaps.length); @@ -38,3 +37,6 @@ contract C // ---- // Warning 6368: (706-720): CHC: Out of bounds access happens here. // Warning 6328: (699-730): CHC: Assertion violation happens here. +// Warning 6368: (920-936): CHC: Out of bounds access happens here. +// Warning 6368: (920-939): CHC: Out of bounds access happens here. +// Warning 6328: (913-949): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/array_static_aliasing_memory_5.sol b/test/libsolidity/smtCheckerTests/types/array_static_aliasing_memory_5.sol index 15b7aed31..7c3562dd9 100644 --- a/test/libsolidity/smtCheckerTests/types/array_static_aliasing_memory_5.sol +++ b/test/libsolidity/smtCheckerTests/types/array_static_aliasing_memory_5.sol @@ -8,8 +8,7 @@ contract C require(a[0] == 2); b[0] = 1; // Should fail since b == c is possible. - // Removed because current Spacer seg faults in cex generation. - //assert(c[0] == 42); + assert(c[0] == 42); // Should fail since b == a is possible. // Access is safe but oob is reported due of aliasing. assert(a[0] == 2); @@ -19,5 +18,7 @@ contract C // ==== // SMTEngine: all // ---- -// Warning 6368: (467-471): CHC: Out of bounds access happens here. -// Warning 6328: (460-477): CHC: Assertion violation happens here. +// Warning 6368: (277-281): CHC: Out of bounds access happens here. +// Warning 6328: (270-288): CHC: Assertion violation happens here. +// Warning 6368: (399-403): CHC: Out of bounds access happens here. +// Warning 6328: (392-409): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/array_static_aliasing_storage_5.sol b/test/libsolidity/smtCheckerTests/types/array_static_aliasing_storage_5.sol index 8841942d7..ac8d09776 100644 --- a/test/libsolidity/smtCheckerTests/types/array_static_aliasing_storage_5.sol +++ b/test/libsolidity/smtCheckerTests/types/array_static_aliasing_storage_5.sol @@ -11,8 +11,7 @@ contract C // erase knowledge about memory references. assert(c[0] == 42); // Fails because b1 == a is possible. - // Disabled because Spacer seg faults. - //assert(a[0] == 2); + assert(a[0] == 2); assert(b1[0] == 1); } function g(bool x, uint[2] memory c) public { @@ -25,7 +24,9 @@ contract C // SMTIgnoreCex: yes // ---- // Warning 6368: (165-169): CHC: Out of bounds access happens here. -// Warning 6368: (178-182): CHC: Out of bounds access happens here. +// Warning 6368: (178-182): CHC: Out of bounds access might happen here. // Warning 6368: (190-195): CHC: Out of bounds access happens here. // Warning 6368: (314-318): CHC: Out of bounds access happens here. -// Warning 6368: (440-445): CHC: Out of bounds access happens here. +// Warning 6368: (376-380): CHC: Out of bounds access happens here. +// Warning 6328: (369-386): CHC: Assertion violation happens here. +// Warning 6368: (397-402): CHC: Out of bounds access happens here. diff --git a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol index 61b7a80f2..619032353 100644 --- a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol +++ b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol @@ -15,8 +15,7 @@ contract C // Should not fail since knowledge is erased only for mapping (uint => uint). assert(severalMaps8[0][0] == 42); // Should fail since map == severalMaps3d[0][0] is possible. - // Removed because current Spacer seg faults in cex generation. - //assert(severalMaps3d[0][0][0] == 42); + assert(severalMaps3d[0][0][0] == 42); } function g(uint x) public { require(x < severalMaps.length); @@ -31,3 +30,6 @@ contract C // Warning 6368: (353-372): CHC: Out of bounds access happens here. // Warning 6368: (463-477): CHC: Out of bounds access happens here. // Warning 6328: (456-487): CHC: Assertion violation happens here. +// Warning 6368: (677-693): CHC: Out of bounds access happens here. +// Warning 6368: (677-696): CHC: Out of bounds access happens here. +// Warning 6328: (670-706): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/mapping_aliasing_2.sol b/test/libsolidity/smtCheckerTests/types/mapping_aliasing_2.sol index 79c03a7d5..6bfc31122 100644 --- a/test/libsolidity/smtCheckerTests/types/mapping_aliasing_2.sol +++ b/test/libsolidity/smtCheckerTests/types/mapping_aliasing_2.sol @@ -14,8 +14,7 @@ contract C // Fails because map2 == a is possible. assert(a[0] == 42); // Fails because map2 == maps[0] is possible. - // Removed because current Spacer seg faults in cex generation. - //assert(maps[0][0] == 42); + assert(maps[0][0] == 42); // Should not fail since knowledge is erased only for mapping (uint => uint). assert(maps8[0][0] == 42); assert(map2[0] == 1); @@ -34,3 +33,4 @@ contract C // ---- // Warning 6328: (364-384): CHC: Assertion violation happens here. // Warning 6328: (430-448): CHC: Assertion violation happens here. +// Warning 6328: (500-524): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol b/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol index a6ec06ba1..900eaeffa 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol @@ -13,25 +13,25 @@ contract C { } function f(S memory s2) public pure { S[] memory s1 = new S[](3); - // Removed because current Spacer seg faults in cex generation. - //assert(s1.length == 3); + assert(s1.length == 3); // should hold s1[0].x = 2; - // Removed because current Spacer seg faults in cex generation. - //assert(s1[0].x == s2.x); + assert(s1[0].x == s2.x); // should fail s1[1].t.y = 3; - // Removed because current Spacer seg faults in cex generation. - //assert(s1[1].t.y == s2.t.y); + assert(s1[1].t.y == s2.t.y); // should fail s1[2].a = new uint[](3); s1[2].a[2] = 4; - // Removed because current Spacer seg faults in cex generation. - //assert(s1[2].a[2] == s2.a[2]); + assert(s1[2].a[2] == s2.a[2]); // should fail s1[0].ts = new T[](4); s1[0].ts[3].y = 5; - // Removed because current Spacer seg faults in cex generation. - //assert(s1[0].ts[3].y == s2.ts[3].y); + assert(s1[0].ts[3].y == s2.ts[3].y); // should fail } } // ==== // SMTEngine: all // ---- -// Warning 5667: (151-162): Unused function parameter. Remove or comment out the variable name to silence this warning. +// Warning 6328: (266-289): CHC: Assertion violation happens here. +// Warning 6328: (325-352): CHC: Assertion violation happens here. +// Warning 6368: (437-444): CHC: Out of bounds access happens here. +// Warning 6328: (416-445): CHC: Assertion violation happens here. +// Warning 6368: (534-542): CHC: Out of bounds access happens here. +// Warning 6328: (510-545): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_storage.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_storage.sol index 4c13699e2..a28b3a637 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_storage.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_storage.sol @@ -7,9 +7,8 @@ contract C { S s2; function f(bool b) public { S storage s3 = b ? s1 : s2; - // Disabled because Spacer 4.8.9 seg fauts. - //assert(s3.x == s1.x); - //assert(s3.x == s2.x); + assert(s3.x == s1.x); + assert(s3.x == s2.x); // This is safe. assert(s3.x == s1.x || s3.x == s2.x); // This fails as false positive because of lack of support to aliasing. @@ -26,4 +25,6 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (369-405): CHC: Assertion violation happens here.\nCounterexample:\ns1 = {x: 0, a: []}, s2 = {x: 0, a: []}\nb = false\ns3 = {x: 42, a: []}\n\nTransaction trace:\nC.constructor()\nState: s1 = {x: 0, a: []}, s2 = {x: 0, a: []}\nC.f(false) +// Warning 6328: (125-145): CHC: Assertion violation happens here.\nCounterexample:\ns1 = {x: 0, a: []}, s2 = {x: 115792089237316195423570985008687907853269984665640564039457584007913129639897, a: []}\nb = false\ns3 = {x: 115792089237316195423570985008687907853269984665640564039457584007913129639897, a: []}\n\nTransaction trace:\nC.constructor()\nState: s1 = {x: 0, a: []}, s2 = {x: 0, a: []}\nC.g(false, 115792089237316195423570985008687907853269984665640564039457584007913129639897)\nState: s1 = {x: 0, a: []}, s2 = {x: 115792089237316195423570985008687907853269984665640564039457584007913129639897, a: []}\nC.f(false) +// Warning 6328: (149-169): CHC: Assertion violation happens here.\nCounterexample:\ns1 = {x: 0, a: []}, s2 = {x: 7720, a: []}\nb = true\ns3 = {x: 0, a: []}\n\nTransaction trace:\nC.constructor()\nState: s1 = {x: 0, a: []}, s2 = {x: 0, a: []}\nC.g(false, 7720)\nState: s1 = {x: 0, a: []}, s2 = {x: 7720, a: []}\nC.f(true) +// Warning 6328: (319-355): CHC: Assertion violation happens here.\nCounterexample:\ns1 = {x: 0, a: []}, s2 = {x: 0, a: []}\nb = false\ns3 = {x: 42, a: []}\n\nTransaction trace:\nC.constructor()\nState: s1 = {x: 0, a: []}, s2 = {x: 0, a: []}\nC.f(false) diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol index d34eb47ed..f9a20305d 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol @@ -14,27 +14,29 @@ contract C { function f(S memory s2) public pure { S memory s1; s1.x = 2; - // Removed because current Spacer seg faults in cex generation. - //assert(s1.x == s2.x); + assert(s1.x == s2.x); // should fail s1.t.y = 3; - // Removed because current Spacer seg faults in cex generation. - //assert(s1.t.y == s2.t.y); + assert(s1.t.y == s2.t.y); // should fail s1.a = new uint[](3); s1.a[2] = 4; - // Removed because current Spacer seg faults in cex generation. - //assert(s1.a[2] == s2.a[2]); + assert(s1.a[2] == s2.a[2]); // should fail s1.ts = new T[](6); s1.ts[3].y = 5; - // Removed because current Spacer seg faults in cex generation. - //assert(s1.ts[3].y == s2.ts[3].y); + assert(s1.ts[3].y == s2.ts[3].y); // should fail s1.ts[4].a = new uint[](6); s1.ts[4].a[5] = 6; require(s2.ts.length > 4); require(s2.ts[4].a.length > 6); - assert(s1.ts[4].a[5] == s2.ts[4].a[5]); + assert(s1.ts[4].a[5] == s2.ts[4].a[5]); // should fail } } // ==== // SMTEngine: all // ---- -// Warning 6328: (804-842): CHC: Assertion violation happens here. +// Warning 6328: (207-227): CHC: Assertion violation happens here. +// Warning 6328: (260-284): CHC: Assertion violation happens here. +// Warning 6368: (360-367): CHC: Out of bounds access happens here. +// Warning 6328: (342-368): CHC: Assertion violation happens here. +// Warning 6368: (448-456): CHC: Out of bounds access happens here. +// Warning 6328: (427-459): CHC: Assertion violation happens here. +// Warning 6328: (592-630): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_mapping.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_mapping.sol index 0ebb38c3d..46d197c56 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_mapping.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_mapping.sol @@ -6,8 +6,7 @@ contract C { S s1; S s2; function f() public view { - // Disabled because Spacer 4.8.9 seg faults. - //assert(s1.m[0] == s2.m[0]); + assert(s1.m[0] == s2.m[0]); } function g(uint a, uint b) public { s1.m[a] = b; @@ -16,3 +15,4 @@ contract C { // ==== // SMTEngine: all // ---- +// Warning 6328: (110-136): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_3.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_3.sol index 67740db93..4830e51a1 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_3.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_3.sol @@ -14,10 +14,9 @@ contract C { require(s1.a[0].a.length > 0); require(s2.a[0].a.length > 0); assert(s1.a[0].a.length == s2.a[0].a.length); - // Disabled because of Spacer killed. - //require(s1.a[0].a[0].a.length > 0); - //require(s2.a[0].a[0].a.length > 0); - //assert(s1.a[0].a[0].x == s2.a[0].a[0].x); + require(s1.a[0].a[0].a.length > 0); + require(s2.a[0].a[0].a.length > 0); + assert(s1.a[0].a[0].x == s2.a[0].a[0].x); } function g() public { s1.x = 42; @@ -73,56 +72,80 @@ contract C { // Warning 7650: (336-340): Assertion checker does not yet support this expression. // Warning 8364: (336-338): Assertion checker does not yet implement type struct C.S storage ref // Warning 8364: (336-343): Assertion checker does not yet implement type struct C.S storage ref -// Warning 7650: (549-553): Assertion checker does not yet support this expression. -// Warning 8364: (549-551): Assertion checker does not yet implement type struct C.S storage ref -// Warning 4375: (549-553): Assertion checker does not support recursive structs. -// Warning 7650: (562-566): Assertion checker does not yet support this expression. -// Warning 8364: (562-564): Assertion checker does not yet implement type struct C.S storage ref -// Warning 4375: (562-566): Assertion checker does not support recursive structs. -// Warning 7650: (575-579): Assertion checker does not yet support this expression. -// Warning 8364: (575-577): Assertion checker does not yet implement type struct C.S storage ref -// Warning 8364: (575-586): Assertion checker does not yet implement type struct C.S storage ref -// Warning 4375: (575-579): Assertion checker does not support recursive structs. -// Warning 7650: (590-594): Assertion checker does not yet support this expression. -// Warning 8364: (590-592): Assertion checker does not yet implement type struct C.S storage ref -// Warning 8364: (590-601): Assertion checker does not yet implement type struct C.S storage ref -// Warning 4375: (590-594): Assertion checker does not support recursive structs. -// Warning 7650: (605-614): Assertion checker does not yet support this expression. -// Warning 7650: (605-609): Assertion checker does not yet support this expression. -// Warning 8364: (605-607): Assertion checker does not yet implement type struct C.S storage ref -// Warning 8364: (605-612): Assertion checker does not yet implement type struct C.S storage ref -// Warning 4375: (605-614): Assertion checker does not support recursive structs. -// Warning 7650: (623-632): Assertion checker does not yet support this expression. -// Warning 7650: (623-627): Assertion checker does not yet support this expression. -// Warning 8364: (623-625): Assertion checker does not yet implement type struct C.S storage ref -// Warning 8364: (623-630): Assertion checker does not yet implement type struct C.S storage ref -// Warning 4375: (623-632): Assertion checker does not support recursive structs. -// Warning 7650: (641-650): Assertion checker does not yet support this expression. -// Warning 7650: (641-645): Assertion checker does not yet support this expression. -// Warning 8364: (641-643): Assertion checker does not yet implement type struct C.S storage ref -// Warning 8364: (641-648): Assertion checker does not yet implement type struct C.S storage ref -// Warning 8364: (641-657): Assertion checker does not yet implement type struct C.S storage ref -// Warning 4375: (641-650): Assertion checker does not support recursive structs. -// Warning 7650: (661-670): Assertion checker does not yet support this expression. -// Warning 7650: (661-665): Assertion checker does not yet support this expression. -// Warning 8364: (661-663): Assertion checker does not yet implement type struct C.S storage ref -// Warning 8364: (661-668): Assertion checker does not yet implement type struct C.S storage ref -// Warning 8364: (661-677): Assertion checker does not yet implement type struct C.S storage ref -// Warning 4375: (661-670): Assertion checker does not support recursive structs. -// Warning 7650: (681-695): Assertion checker does not yet support this expression. -// Warning 7650: (681-690): Assertion checker does not yet support this expression. -// Warning 7650: (681-685): Assertion checker does not yet support this expression. -// Warning 8364: (681-683): Assertion checker does not yet implement type struct C.S storage ref -// Warning 8364: (681-688): Assertion checker does not yet implement type struct C.S storage ref -// Warning 8364: (681-693): Assertion checker does not yet implement type struct C.S storage ref -// Warning 4375: (681-695): Assertion checker does not support recursive structs. -// Warning 7650: (704-718): Assertion checker does not yet support this expression. -// Warning 7650: (704-713): Assertion checker does not yet support this expression. -// Warning 7650: (704-708): Assertion checker does not yet support this expression. -// Warning 8364: (704-706): Assertion checker does not yet implement type struct C.S storage ref -// Warning 8364: (704-711): Assertion checker does not yet implement type struct C.S storage ref -// Warning 8364: (704-716): Assertion checker does not yet implement type struct C.S storage ref -// Warning 4375: (704-718): Assertion checker does not support recursive structs. +// Warning 7650: (365-379): Assertion checker does not yet support this expression. +// Warning 7650: (365-374): Assertion checker does not yet support this expression. +// Warning 7650: (365-369): Assertion checker does not yet support this expression. +// Warning 8364: (365-367): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (365-372): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (365-377): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (403-417): Assertion checker does not yet support this expression. +// Warning 7650: (403-412): Assertion checker does not yet support this expression. +// Warning 7650: (403-407): Assertion checker does not yet support this expression. +// Warning 8364: (403-405): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (403-410): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (403-415): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (440-454): Assertion checker does not yet support this expression. +// Warning 7650: (440-449): Assertion checker does not yet support this expression. +// Warning 7650: (440-444): Assertion checker does not yet support this expression. +// Warning 8364: (440-442): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (440-447): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (440-452): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (458-472): Assertion checker does not yet support this expression. +// Warning 7650: (458-467): Assertion checker does not yet support this expression. +// Warning 7650: (458-462): Assertion checker does not yet support this expression. +// Warning 8364: (458-460): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (458-465): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (458-470): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (503-507): Assertion checker does not yet support this expression. +// Warning 8364: (503-505): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (503-507): Assertion checker does not support recursive structs. +// Warning 7650: (516-520): Assertion checker does not yet support this expression. +// Warning 8364: (516-518): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (516-520): Assertion checker does not support recursive structs. +// Warning 7650: (529-533): Assertion checker does not yet support this expression. +// Warning 8364: (529-531): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (529-540): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (529-533): Assertion checker does not support recursive structs. +// Warning 7650: (544-548): Assertion checker does not yet support this expression. +// Warning 8364: (544-546): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (544-555): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (544-548): Assertion checker does not support recursive structs. +// Warning 7650: (559-568): Assertion checker does not yet support this expression. +// Warning 7650: (559-563): Assertion checker does not yet support this expression. +// Warning 8364: (559-561): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (559-566): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (559-568): Assertion checker does not support recursive structs. +// Warning 7650: (577-586): Assertion checker does not yet support this expression. +// Warning 7650: (577-581): Assertion checker does not yet support this expression. +// Warning 8364: (577-579): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (577-584): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (577-586): Assertion checker does not support recursive structs. +// Warning 7650: (595-604): Assertion checker does not yet support this expression. +// Warning 7650: (595-599): Assertion checker does not yet support this expression. +// Warning 8364: (595-597): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (595-602): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (595-611): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (595-604): Assertion checker does not support recursive structs. +// Warning 7650: (615-624): Assertion checker does not yet support this expression. +// Warning 7650: (615-619): Assertion checker does not yet support this expression. +// Warning 8364: (615-617): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (615-622): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (615-631): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (615-624): Assertion checker does not support recursive structs. +// Warning 7650: (635-649): Assertion checker does not yet support this expression. +// Warning 7650: (635-644): Assertion checker does not yet support this expression. +// Warning 7650: (635-639): Assertion checker does not yet support this expression. +// Warning 8364: (635-637): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (635-642): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (635-647): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (635-649): Assertion checker does not support recursive structs. +// Warning 7650: (658-672): Assertion checker does not yet support this expression. +// Warning 7650: (658-667): Assertion checker does not yet support this expression. +// Warning 7650: (658-662): Assertion checker does not yet support this expression. +// Warning 8364: (658-660): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (658-665): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (658-670): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (658-672): Assertion checker does not support recursive structs. // Warning 6328: (91-111): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() // Warning 6328: (115-149): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() // Warning 6368: (216-223): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() @@ -133,14 +156,23 @@ contract C { // Warning 6368: (316-323): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() // Warning 6368: (336-343): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() // Warning 6328: (309-353): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() -// Warning 6368: (605-612): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g() -// Warning 6368: (623-630): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g() -// Warning 6368: (641-648): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g() -// Warning 6368: (661-668): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g() -// Warning 6368: (681-688): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g() -// Warning 6368: (681-693): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g() -// Warning 6368: (704-711): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g() -// Warning 6368: (704-716): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g() +// Warning 6368: (365-372): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6368: (365-377): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6368: (403-410): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6368: (403-415): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6368: (440-447): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6368: (440-452): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6368: (458-465): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6368: (458-470): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (433-473): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6368: (559-566): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g() +// Warning 6368: (577-584): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g() +// Warning 6368: (595-602): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g() +// Warning 6368: (615-622): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g() +// Warning 6368: (635-642): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g() +// Warning 6368: (635-647): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g() +// Warning 6368: (658-665): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g() +// Warning 6368: (658-670): CHC: Out of bounds access happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g() // Warning 8115: (48-52): Assertion checker does not yet support the type of this variable. // Warning 8115: (55-59): Assertion checker does not yet support the type of this variable. // Warning 7650: (98-102): Assertion checker does not yet support this expression. @@ -179,53 +211,77 @@ contract C { // Warning 7650: (336-340): Assertion checker does not yet support this expression. // Warning 8364: (336-338): Assertion checker does not yet implement type struct C.S storage ref // Warning 8364: (336-343): Assertion checker does not yet implement type struct C.S storage ref -// Warning 7650: (549-553): Assertion checker does not yet support this expression. -// Warning 8364: (549-551): Assertion checker does not yet implement type struct C.S storage ref -// Warning 4375: (549-553): Assertion checker does not support recursive structs. -// Warning 7650: (562-566): Assertion checker does not yet support this expression. -// Warning 8364: (562-564): Assertion checker does not yet implement type struct C.S storage ref -// Warning 4375: (562-566): Assertion checker does not support recursive structs. -// Warning 7650: (575-579): Assertion checker does not yet support this expression. -// Warning 8364: (575-577): Assertion checker does not yet implement type struct C.S storage ref -// Warning 8364: (575-586): Assertion checker does not yet implement type struct C.S storage ref -// Warning 4375: (575-579): Assertion checker does not support recursive structs. -// Warning 7650: (590-594): Assertion checker does not yet support this expression. -// Warning 8364: (590-592): Assertion checker does not yet implement type struct C.S storage ref -// Warning 8364: (590-601): Assertion checker does not yet implement type struct C.S storage ref -// Warning 4375: (590-594): Assertion checker does not support recursive structs. -// Warning 7650: (605-614): Assertion checker does not yet support this expression. -// Warning 7650: (605-609): Assertion checker does not yet support this expression. -// Warning 8364: (605-607): Assertion checker does not yet implement type struct C.S storage ref -// Warning 8364: (605-612): Assertion checker does not yet implement type struct C.S storage ref -// Warning 4375: (605-614): Assertion checker does not support recursive structs. -// Warning 7650: (623-632): Assertion checker does not yet support this expression. -// Warning 7650: (623-627): Assertion checker does not yet support this expression. -// Warning 8364: (623-625): Assertion checker does not yet implement type struct C.S storage ref -// Warning 8364: (623-630): Assertion checker does not yet implement type struct C.S storage ref -// Warning 4375: (623-632): Assertion checker does not support recursive structs. -// Warning 7650: (641-650): Assertion checker does not yet support this expression. -// Warning 7650: (641-645): Assertion checker does not yet support this expression. -// Warning 8364: (641-643): Assertion checker does not yet implement type struct C.S storage ref -// Warning 8364: (641-648): Assertion checker does not yet implement type struct C.S storage ref -// Warning 8364: (641-657): Assertion checker does not yet implement type struct C.S storage ref -// Warning 4375: (641-650): Assertion checker does not support recursive structs. -// Warning 7650: (661-670): Assertion checker does not yet support this expression. -// Warning 7650: (661-665): Assertion checker does not yet support this expression. -// Warning 8364: (661-663): Assertion checker does not yet implement type struct C.S storage ref -// Warning 8364: (661-668): Assertion checker does not yet implement type struct C.S storage ref -// Warning 8364: (661-677): Assertion checker does not yet implement type struct C.S storage ref -// Warning 4375: (661-670): Assertion checker does not support recursive structs. -// Warning 7650: (681-695): Assertion checker does not yet support this expression. -// Warning 7650: (681-690): Assertion checker does not yet support this expression. -// Warning 7650: (681-685): Assertion checker does not yet support this expression. -// Warning 8364: (681-683): Assertion checker does not yet implement type struct C.S storage ref -// Warning 8364: (681-688): Assertion checker does not yet implement type struct C.S storage ref -// Warning 8364: (681-693): Assertion checker does not yet implement type struct C.S storage ref -// Warning 4375: (681-695): Assertion checker does not support recursive structs. -// Warning 7650: (704-718): Assertion checker does not yet support this expression. -// Warning 7650: (704-713): Assertion checker does not yet support this expression. -// Warning 7650: (704-708): Assertion checker does not yet support this expression. -// Warning 8364: (704-706): Assertion checker does not yet implement type struct C.S storage ref -// Warning 8364: (704-711): Assertion checker does not yet implement type struct C.S storage ref -// Warning 8364: (704-716): Assertion checker does not yet implement type struct C.S storage ref -// Warning 4375: (704-718): Assertion checker does not support recursive structs. +// Warning 7650: (365-379): Assertion checker does not yet support this expression. +// Warning 7650: (365-374): Assertion checker does not yet support this expression. +// Warning 7650: (365-369): Assertion checker does not yet support this expression. +// Warning 8364: (365-367): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (365-372): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (365-377): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (403-417): Assertion checker does not yet support this expression. +// Warning 7650: (403-412): Assertion checker does not yet support this expression. +// Warning 7650: (403-407): Assertion checker does not yet support this expression. +// Warning 8364: (403-405): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (403-410): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (403-415): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (440-454): Assertion checker does not yet support this expression. +// Warning 7650: (440-449): Assertion checker does not yet support this expression. +// Warning 7650: (440-444): Assertion checker does not yet support this expression. +// Warning 8364: (440-442): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (440-447): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (440-452): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (458-472): Assertion checker does not yet support this expression. +// Warning 7650: (458-467): Assertion checker does not yet support this expression. +// Warning 7650: (458-462): Assertion checker does not yet support this expression. +// Warning 8364: (458-460): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (458-465): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (458-470): Assertion checker does not yet implement type struct C.S storage ref +// Warning 7650: (503-507): Assertion checker does not yet support this expression. +// Warning 8364: (503-505): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (503-507): Assertion checker does not support recursive structs. +// Warning 7650: (516-520): Assertion checker does not yet support this expression. +// Warning 8364: (516-518): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (516-520): Assertion checker does not support recursive structs. +// Warning 7650: (529-533): Assertion checker does not yet support this expression. +// Warning 8364: (529-531): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (529-540): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (529-533): Assertion checker does not support recursive structs. +// Warning 7650: (544-548): Assertion checker does not yet support this expression. +// Warning 8364: (544-546): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (544-555): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (544-548): Assertion checker does not support recursive structs. +// Warning 7650: (559-568): Assertion checker does not yet support this expression. +// Warning 7650: (559-563): Assertion checker does not yet support this expression. +// Warning 8364: (559-561): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (559-566): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (559-568): Assertion checker does not support recursive structs. +// Warning 7650: (577-586): Assertion checker does not yet support this expression. +// Warning 7650: (577-581): Assertion checker does not yet support this expression. +// Warning 8364: (577-579): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (577-584): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (577-586): Assertion checker does not support recursive structs. +// Warning 7650: (595-604): Assertion checker does not yet support this expression. +// Warning 7650: (595-599): Assertion checker does not yet support this expression. +// Warning 8364: (595-597): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (595-602): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (595-611): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (595-604): Assertion checker does not support recursive structs. +// Warning 7650: (615-624): Assertion checker does not yet support this expression. +// Warning 7650: (615-619): Assertion checker does not yet support this expression. +// Warning 8364: (615-617): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (615-622): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (615-631): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (615-624): Assertion checker does not support recursive structs. +// Warning 7650: (635-649): Assertion checker does not yet support this expression. +// Warning 7650: (635-644): Assertion checker does not yet support this expression. +// Warning 7650: (635-639): Assertion checker does not yet support this expression. +// Warning 8364: (635-637): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (635-642): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (635-647): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (635-649): Assertion checker does not support recursive structs. +// Warning 7650: (658-672): Assertion checker does not yet support this expression. +// Warning 7650: (658-667): Assertion checker does not yet support this expression. +// Warning 7650: (658-662): Assertion checker does not yet support this expression. +// Warning 8364: (658-660): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (658-665): Assertion checker does not yet implement type struct C.S storage ref +// Warning 8364: (658-670): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4375: (658-672): Assertion checker does not support recursive structs. diff --git a/test/libsolidity/smtCheckerTests/types/struct_array_branches_3d.sol b/test/libsolidity/smtCheckerTests/types/struct_array_branches_3d.sol index dbd498327..3006a271e 100644 --- a/test/libsolidity/smtCheckerTests/types/struct_array_branches_3d.sol +++ b/test/libsolidity/smtCheckerTests/types/struct_array_branches_3d.sol @@ -10,17 +10,16 @@ contract C assert(c.a[0].length == 2); assert(c.a[0][0].length == 0); c.a[0][0] = new uint[](2); - // Disabled because of Spacer's seg fault. - /* if (b) c.a[0][0][0] = 1; else c.a[0][0][0] = 2; assert(c.a[0][0][0] > 0); - */ } } // ==== // SMTEngine: all // ---- -// Warning 5667: (53-59): Unused function parameter. Remove or comment out the variable name to silence this warning. +// Warning 6368: (360-369): CHC: Out of bounds access might happen here. +// Warning 6368: (360-372): CHC: Out of bounds access might happen here. +// Warning 6328: (353-377): CHC: Assertion violation might happen here.