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

Merge pull request #9774 from ethereum/smt_remove_test

Browse Source 
Adjust problematic SMTChecker tests
This commit is contained in:
chriseth 2020-09-11 10:32:11 +02:00 committed by GitHub
commit 61d2a18422
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 0 additions and 43 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -22,8 +22,6 @@ 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]);
}
}
// ----
@ -31,5 +29,4 @@ 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,8 +22,6 @@ 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);
}
}
// ----
@ -31,4 +29,3 @@ 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
View File

@ -1,34 +0,0 @@
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,8 +21,6 @@ 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);
}
}
// ----
@ -30,4 +28,3 @@ 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.