cerc-io/solidity
16
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

Readd SMTChecker tests

Browse Source
This commit is contained in:
Leonardo Alt 2020-09-14 23:38:31 +02:00
parent 552a5f0913
commit 28c8e01149
10 changed files with 103 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
test/libsolidity/smtCheckerTests/invariants/loop_nested.sol
View File

@ -1,8 +1,5 @@
pragma experimental SMTChecker;
// This test gets different results on Linux and OSX.
// Re-enable when fixed (SMTSolvers: z3)
contract Simple {
function f() public pure {
uint x = 10;
@ -18,8 +15,4 @@ contract Simple {
assert(y == x);
}
}
// ====
// SMTSolvers: none
// ----
// Warning: (195-209): Error trying to invoke SMT solver.
// Warning: (195-209): Assertion violation happens here

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

@ -13,8 +13,6 @@ contract C
assert(x > 0);
}
}
// ====
// SMTSolvers: cvc4
// ----
// Warning 1218: (176-181): Error trying to invoke SMT solver.
// Warning 2661: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4661: (296-309): Assertion violation happens here.

8
test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol
View File

@ -20,9 +20,7 @@ contract LoopFor2 {
assert(b[0] == 900);
}
}
// ====
// SMTSolvers: cvc4
// ----
// Warning 4661: (296-316): Assertion violation happens here.
// Warning 4661: (320-339): Assertion violation happens here.
// Warning 4661: (343-362): Assertion violation happens here.
// Warning 1218: (229-234): Error trying to invoke SMT solver.
// Warning 6328: (320-339): Assertion violation happens here.
// Warning 6328: (343-362): Assertion violation happens here.

6
test/libsolidity/smtCheckerTests/operators/delete_multid_array.sol
View File

@ -37,8 +37,6 @@ contract C {
b[x][y] = z;
}
}
// ====
// SMTSolvers: cvc4
// ----
// Warning 4661: (372-392): Assertion violation happens here.
// Warning 4661: (617-637): Assertion violation happens here.
// Warning 6328: (372-392): Assertion violation happens here.
// Warning 6328: (617-637): Assertion violation happens here.

19
test/libsolidity/smtCheckerTests/operators/shifts/shift_right_uint8.sol Normal file
View File

@ -0,0 +1,19 @@
pragma experimental SMTChecker;
contract C {
function f(uint8 a, uint8 b) internal pure returns (uint256) {
return a >> b;
}
function t() public pure {
assert(f(0x66, 0) == 0x66);
// Fails because the above is true.
assert(f(0x66, 0) == 0x6);
assert(f(0x66, 8) == 0);
// Fails because the above is true.
assert(f(0x66, 8) == 1);
}
}
// ----
// Warning 6328: (240-265): Assertion violation happens here.
// Warning 6328: (335-358): Assertion violation happens here.

35
test/libsolidity/smtCheckerTests/types/mapping_aliasing_2.sol Normal file
View File

@ -0,0 +1,35 @@
pragma experimental SMTChecker;
contract C
{
mapping (uint => uint) a;
mapping (uint => mapping (uint => uint)) maps;
mapping (uint => mapping (uint => uint8)) maps8;
function f(mapping (uint => uint) storage map1, mapping (uint => uint) storage map2) internal {
map1[0] = 2;
a[0] = 42;
maps[0][0] = 42;
maps8[0][0] = 42;
map2[0] = 1;
// Fails because map2 == map1 is possible.
assert(map1[0] == 2);
// Fails because map2 == a is possible.
assert(a[0] == 42);
// Fails because map2 == maps[0] is possible.
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);
}
function g(bool b, uint x, uint y) public {
if (b)
f(a, maps[y]);
else
f(maps[x], maps[y]);
}
}
// ----
// Warning 6328: (397-417): Assertion violation happens here.
// Warning 6328: (463-481): Assertion violation happens here.
// Warning 6328: (533-557): Assertion violation happens here.

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

@ -22,6 +22,8 @@ contract C {
assert(s1[2].a[2] == s2.a[2]);
s1[0].ts[3].y = 5;
assert(s1[0].ts[3].y == s2.ts[3].y);
s1[1].ts[4].a[5] = 6;
assert(s1[1].ts[4].a[5] == s2.ts[4].a[5]);
}
}
// ----
@ -29,4 +31,5 @@ contract C {
// Warning 6328: (301-328): Assertion violation happens here.
// Warning 6328: (350-379): Assertion violation happens here.
// Warning 6328: (404-439): Assertion violation happens here.
// Warning 6328: (467-508): Assertion violation happens here.
// Warning 4588: (228-238): Assertion checker does not yet implement this type of function call.

3
test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_1.sol
View File

@ -22,6 +22,8 @@ contract C {
assert(s1.a[2] != 4);
s1.ts[3].y = 5;
assert(s1.ts[3].y != 5);
s1.ts[4].a[5] = 6;
assert(s1.ts[4].a[5] != 6);
}
}
// ----
@ -29,3 +31,4 @@ contract C {
// Warning 6328: (263-282): Assertion violation happens here.
// Warning 6328: (301-321): Assertion violation happens here.
// Warning 6328: (343-366): Assertion violation happens here.
// Warning 6328: (391-417): Assertion violation happens here.

34
test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol Normal file
View File

@ -0,0 +1,34 @@
pragma experimental SMTChecker;
pragma experimental ABIEncoderV2;
contract C {
struct T {
uint y;
uint[] a;
}
struct S {
uint x;
T t;
uint[] a;
T[] ts;
}
function f(S memory s2) public pure {
S memory s1;
s1.x = 2;
assert(s1.x == s2.x);
s1.t.y = 3;
assert(s1.t.y == s2.t.y);
s1.a[2] = 4;
assert(s1.a[2] == s2.a[2]);
s1.ts[3].y = 5;
assert(s1.ts[3].y == s2.ts[3].y);
s1.ts[4].a[5] = 6;
assert(s1.ts[4].a[5] == s2.ts[4].a[5]);
}
}
// ----
// Warning 6328: (239-259): Assertion violation happens here.
// Warning 6328: (277-301): Assertion violation happens here.
// Warning 6328: (320-346): Assertion violation happens here.
// Warning 6328: (368-400): Assertion violation happens here.
// Warning 6328: (425-463): Assertion violation happens here.

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

@ -21,6 +21,8 @@ contract C {
assert(s1.a[2] != 4);
s1.ts[3].y = 5;
assert(s1.ts[3].y != 5);
s1.ts[4].a[5] = 6;
assert(s1.ts[4].a[5] != 6);
}
}
// ----
@ -28,3 +30,4 @@ contract C {
// Warning 6328: (216-235): Assertion violation happens here.
// Warning 6328: (254-274): Assertion violation happens here.
// Warning 6328: (296-319): Assertion violation happens here.
// Warning 6328: (344-370): Assertion violation happens here.