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

updates to the tests

Browse Source
This commit is contained in:
Martin Blicha 2020-12-18 19:10:32 +01:00
parent f76ff35225
commit 745466b71f
21 changed files with 140 additions and 45 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_array_slice_2.sol
View File

@ -12,13 +12,15 @@ contract C {
//assert(b1.length == b3.length); // fails for now
bytes memory b4 = abi.encodePacked(data[5:10]);
assert(b1.length == b4.length); // should fail
// Disabled because of Spacer nondeterminism
//assert(b1.length == b4.length); // should fail
uint x = 5;
uint y = 10;
bytes memory b5 = abi.encodePacked(data[x:y]);
// Disabled because of Spacer nondeterminism
//uint x = 5;
//uint y = 10;
//bytes memory b5 = abi.encodePacked(data[x:y]);
// should hold but the engine cannot infer that data[5:10] is fully equals data[x:y] because each index is assigned separately
assert(b1.length == b5.length); // fails for now
//assert(b1.length == b5.length); // fails for now
bytes memory b6 = abi.encode(data[5:10]);
assert(b4.length == b6.length); // should fail
@ -26,12 +28,4 @@ contract C {
}
// ----
// Warning 6328: (330-360): CHC: Assertion violation happens here.
// Warning 1218: (725-755): CHC: Error trying to invoke SMT solver.
// Warning 6328: (725-755): CHC: Assertion violation might happen here.
// Warning 1218: (982-1012): CHC: Error trying to invoke SMT solver.
// Warning 6328: (982-1012): CHC: Assertion violation might happen here.
// Warning 1218: (1078-1108): CHC: Error trying to invoke SMT solver.
// Warning 6328: (1078-1108): CHC: Assertion violation might happen here.
// Warning 4661: (725-755): BMC: Assertion violation happens here.
// Warning 4661: (982-1012): BMC: Assertion violation happens here.
// Warning 4661: (1078-1108): BMC: Assertion violation happens here.
// Warning 6328: (1182-1212): CHC: Assertion violation happens here.

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

@ -16,8 +16,9 @@ contract C {
assert(b1.length != b5.length); // should fail
assert(b1.length == b5.length); // should fail
bytes memory b6 = abi.encode(x, z, a);
assert(b1.length == b6.length); // should fail
// Commented out because of nondeterminism in Spacer in Z3 4.8.9
//bytes memory b6 = abi.encode(x, z, a);
//assert(b1.length == b6.length); // should fail
}
}
// ----
@ -28,7 +29,6 @@ contract C {
// Warning 6328: (560-590): CHC: Assertion violation might happen here.
// Warning 1218: (609-639): CHC: Error trying to invoke SMT solver.
// Warning 6328: (609-639): CHC: Assertion violation might happen here.
// Warning 6328: (700-730): CHC: Assertion violation happens here.
// Warning 4661: (451-481): BMC: Assertion violation happens here.
// Warning 4661: (560-590): BMC: Assertion violation happens here.
// Warning 4661: (609-639): BMC: Assertion violation happens here.

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

@ -6,8 +6,9 @@ contract C {
bytes memory b2 = abi.encodeWithSignature(sig, y, z, a);
assert(b1.length == b2.length);
bytes memory b3 = abi.encodeWithSignature(sig, y, z, b);
assert(b1.length == b3.length); // should fail
// Disabled because of nondeterminism in Spacer Z3 4.8.9
//bytes memory b3 = abi.encodeWithSignature(sig, y, z, b);
//assert(b1.length == b3.length); // should fail
bytes memory b4 = abi.encodeWithSignature(sig, t, z, a);
assert(b1.length == b4.length); // should fail
@ -21,14 +22,10 @@ contract C {
}
}
// ----
// Warning 6328: (403-433): CHC: Assertion violation happens here.
// Warning 6328: (512-542): CHC: Assertion violation happens here.
// Warning 1218: (633-663): CHC: Error trying to invoke SMT solver.
// Warning 6328: (633-663): CHC: Assertion violation might happen here.
// Warning 1218: (682-712): CHC: Error trying to invoke SMT solver.
// Warning 6328: (682-712): CHC: Assertion violation might happen here.
// Warning 1218: (793-823): CHC: Error trying to invoke SMT solver.
// Warning 6328: (793-823): CHC: Assertion violation might happen here.
// Warning 4661: (633-663): BMC: Assertion violation happens here.
// Warning 4661: (682-712): BMC: Assertion violation happens here.
// Warning 4661: (793-823): BMC: Assertion violation happens here.
// Warning 5667: (139-154): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 6328: (575-605): CHC: Assertion violation happens here.
// Warning 6328: (696-726): CHC: Assertion violation happens here.
// Warning 6328: (745-775): CHC: Assertion violation happens here.
// Warning 1218: (856-886): CHC: Error trying to invoke SMT solver.
// Warning 6328: (856-886): CHC: Assertion violation might happen here.
// Warning 4661: (856-886): BMC: Assertion violation happens here.

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

@ -10,4 +10,4 @@ contract C {
}
}
// ----
// Warning 6328: (199-234): CHC: Assertion violation happens here.\nCounterexample:\n\na = 21238\n\n\nTransaction trace:\nconstructor()\nf(21238)
// Warning 6328: (199-234): CHC: Assertion violation happens here.\nCounterexample:\n\na = 2437\n\n\nTransaction trace:\nconstructor()\nf(2437)

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

@ -17,4 +17,4 @@ contract C {
}
}
// ----
// Warning 6328: (200-214): CHC: Assertion violation happens here.\nCounterexample:\nx = 10, d = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0, d = 0\nf()\nState: x = 1, d = 0\nf()\nState: x = 2, d = 0\ng()
// Warning 6328: (200-214): CHC: Assertion violation happens here.

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

@ -34,4 +34,4 @@ contract C {
}
}
// ----
// Warning 6328: (528-565): CHC: Assertion violation happens here.\nCounterexample:\nowner = 1, y = 0, z = 0, s = 0\n\n\n\nTransaction trace:\nconstructor()\nState: owner = 1, y = 0, z = 0, s = 0\ninv()
// Warning 6328: (528-565): CHC: Assertion violation happens here.\nCounterexample:\nowner = 1, y = 0, z = 0, s = 0\n\n\n\nTransaction trace:\nconstructor()\nState: owner = 1, y = 0, z = 0, s = 0\nf()

1
test/libsolidity/smtCheckerTests/external_calls/external_inc.sol
View File

@ -21,5 +21,6 @@ contract C {
// SMTIgnoreCex: yes
// ----
// Warning 4984: (146-149): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (146-149): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6328: (189-203): CHC: Assertion violation happens here.
// Warning 2661: (146-149): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

19
test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_1.sol Normal file
View File

@ -0,0 +1,19 @@
pragma experimental SMTChecker;
interface D { function e() external; }
contract C {
bool locked = true;
function call(address target) public {
locked = false;
D(target).e();
locked = true;
}
function broken() public view {
assert(locked);
}
}
// ----
// Warning 6328: (239-253): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0\n\n\nTransaction trace:\nconstructor()\nState: locked = true\ncall(0)

16
test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol Normal file
View File

@ -0,0 +1,16 @@
pragma experimental SMTChecker;
interface D { function e() external; }
contract C {
bool locked = true;
function call(address target) public {
assert(locked);
locked = false;
D(target).e();
locked = true;
}
}
// ----
// Warning 6328: (150-164): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0\n\n\nTransaction trace:\nconstructor()\nState: locked = true\ncall(0)

31
test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_3.sol Normal file
View File

@ -0,0 +1,31 @@
pragma experimental SMTChecker;
abstract contract D {
function d() virtual public {}
}
contract A {
int x = 0;
function f() virtual public view {
assert(x == 0); // should hold
assert(x == 1); // should fail
}
}
contract C is A {
constructor() {
x = 1;
}
function call(D d) public {
d.d();
}
function f() public view override {
assert(x == 1); // should hold
assert(x == 0); // should fail
}
}
// ----
// Warning 6328: (187-201): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nf()
// Warning 6328: (385-399): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\nd = 0\n\n\nTransaction trace:\nconstructor()\nState: x = 1\ncall(0)

26
test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_crypto.sol Normal file
View File

@ -0,0 +1,26 @@
pragma experimental SMTChecker;
abstract contract D {
function d() virtual public;
}
contract C {
bytes data;
bytes32 kec;
constructor(bytes memory _data) {
data = _data;
kec = keccak256(data);
}
function f() public view {
bytes32 _kec = keccak256(data);
assert(_kec == kec);
}
function ext(D d) public {
d.d();
}
}

2
test/libsolidity/smtCheckerTests/functions/constructor_state_value_inherited.sol
View File

@ -15,4 +15,4 @@ contract C is B {
}
}
// ----
// Warning 6328: (165-179): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 11\n\n\nTransaction trace:\nconstructor()\nState: x = 10\nf(11)
// Warning 6328: (165-179): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 9\n\n\nTransaction trace:\nconstructor()\nState: x = 10\nf(9)

2
test/libsolidity/smtCheckerTests/functions/constructor_state_value_parameter.sol
View File

@ -14,4 +14,4 @@ contract C {
}
// ----
// Warning 6328: (162-176): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 1\n\n\nTransaction trace:\nconstructor(0, 0)\nState: x = 0\nf(1)
// Warning 4984: (115-120): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nx = 5\na = 115792089237316195423570985008687907853269984665640564039457584007913129639935\nb = 1\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639935, 1)
// Warning 4984: (115-120): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nx = 5\na = 1\nb = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\n\nTransaction trace:\nconstructor(1, 115792089237316195423570985008687907853269984665640564039457584007913129639935)

12
test/libsolidity/smtCheckerTests/functions/functions_external_2.sol
View File

@ -12,10 +12,16 @@ contract C
require(map[0] == map[1]);
assert(map[0] == map[1]);
d.g(y);
// Storage knowledge is cleared after an external call.
assert(map[0] == map[1]);
assert(map[0] == 0); // should fail
}
function set(uint x) public {
map[0] = x;
map[1] = x;
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (297-321): CHC: Assertion violation might happen here.
// Warning 4661: (297-321): BMC: Assertion violation happens here.
// Warning 6328: (267-286): CHC: Assertion violation happens here.

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

@ -18,5 +18,7 @@ contract C {
assert(y == 1); // should fail
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (307-321): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf()
// Warning 6328: (307-321): CHC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol
View File

@ -20,5 +20,4 @@ contract LoopFor2 {
}
// ----
// Warning 4984: (236-241): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 4984: (216-222): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
// Warning 6328: (363-382): CHC: Assertion violation happens here.\nCounterexample:\nb = [], c = []\nn = 1\n\n\nTransaction trace:\nconstructor()\nState: b = [], c = []\ntestUnboundedForLoop(1)

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

@ -13,5 +13,7 @@ contract C {
assert(y[0] == (bytes1("d") | bytes1("e")) ^ bytes1("f"));
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (189-208): CHC: Assertion violation happens here.

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

@ -24,4 +24,4 @@ contract C {
}
// ----
// Warning 2072: (282-288): Unused local variable.
// Warning 6328: (304-328): CHC: Assertion violation happens here.\nCounterexample:\na = false, x = 3, d = 0\n\n\n\nTransaction trace:\nconstructor()\nState: a = false, x = 0, d = 0\nf()
// Warning 6328: (304-328): CHC: Assertion violation happens here.\nCounterexample:\na = false, x = 3, d = 0\n\n = 0\n\nTransaction trace:\nconstructor()\nState: a = false, x = 0, d = 0\ng()

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

@ -14,6 +14,6 @@ contract C
}
}
// ----
// Warning 6328: (295-324): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 100\na = 7719\nb = 7720\n\n\nTransaction trace:\nconstructor()\nf(100, 7719, 7720)
// Warning 6328: (295-324): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 100\na = 7720\nb = 7719\n\n\nTransaction trace:\nconstructor()\nf(100, 7720, 7719)
// Warning 1236: (217-232): BMC: Insufficient funds happens here.
// Warning 1236: (236-251): BMC: Insufficient funds happens here.

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

@ -26,5 +26,7 @@ contract C
assert(b[0] == 1);
}
}
// ====
// SMTIgnoreCex: yes
// ----
// Warning 6328: (572-589): CHC: Assertion violation happens here.

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

@ -2,7 +2,8 @@ pragma experimental SMTChecker;
contract C
{
function f(bool b, uint[] memory c) public {
function f(bool b, uint[] memory c) public pure {
require(c.length <= 2);
c[0] = 0;
if (b)
c[0] = 1;
@ -10,5 +11,4 @@ contract C
}
}
// ----
// Warning 2018: (47-148): Function state mutability can be restricted to pure
// Warning 6328: (128-144): CHC: Assertion violation happens here.\nCounterexample:\n\nb = false\nc = [0, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 18, 14, 14, 21, 14, 14, 23, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14]\n\n\nTransaction trace:\nconstructor()\nf(false, [7719, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 18, 14, 14, 21, 14, 14, 23, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14])
// Warning 6328: (159-175): CHC: Assertion violation happens here.\nCounterexample:\n\nb = false\nc = [0, 5]\n\n\nTransaction trace:\nconstructor()\nf(false, [7719, 5])