cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Enable tests that were killed by oom or seg fault

Browse Source
This commit is contained in:
Leo Alt 2021-07-15 12:49:58 +02:00
parent 3d26d47d46
commit 839bc6f698
29 changed files with 322 additions and 234 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol
View File

@ -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.

4
test/libsolidity/smtCheckerTests/blockchain_state/decreasing_balance.sol
View File

@ -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()

4
test/libsolidity/smtCheckerTests/bmc_coverage/unary_add_minus_overflow_detected.sol
View File

@ -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.

7
test/libsolidity/smtCheckerTests/external_calls/external_inc1_inc2.sol
View File

@ -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.

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

@ -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.

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

@ -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.

4
test/libsolidity/smtCheckerTests/invariants/state_machine_1_fail.sol
View File

@ -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.

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

@ -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.

23
test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_storage.sol
View File

@ -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.

24
test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol
View File

@ -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.

19
test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol
View File

@ -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.

5
test/libsolidity/smtCheckerTests/operators/unary_add_minus_overflow_detected.sol
View File

@ -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.

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

@ -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

9
test/libsolidity/smtCheckerTests/types/array_aliasing_memory_2.sol
View File

@ -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.

8
test/libsolidity/smtCheckerTests/types/array_aliasing_memory_3.sol
View File

@ -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.

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

@ -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.

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

@ -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.

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

@ -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.

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

@ -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.

9
test/libsolidity/smtCheckerTests/types/array_static_aliasing_memory_5.sol
View File

@ -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.

9
test/libsolidity/smtCheckerTests/types/array_static_aliasing_storage_5.sol
View File

@ -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.

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

@ -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.

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

@ -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.

22
test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_memory_unsafe.sol
View File

@ -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.

9
test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_storage.sol
View File

@ -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)

22
test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol
View File

@ -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.

4
test/libsolidity/smtCheckerTests/types/struct/struct_mapping.sol
View File

@ -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.

280
test/libsolidity/smtCheckerTests/types/struct/struct_recursive_3.sol
View File

@ -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.

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

@ -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.