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

Update old tests

Browse Source
This commit is contained in:
Leonardo Alt 2021-03-31 17:11:54 +02:00
parent d617ef461e
commit 0a4afa71bd
1036 changed files with 3950 additions and 3904 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
test/libsolidity/smtCheckerTests/abi/abi_decode_1_tuple.sol
View File

@ -1,11 +1,12 @@
pragma experimental SMTChecker;
contract C {
function f(bytes calldata data) external pure returns (uint256[] memory) {
return abi.decode(data, (uint256[]));
}
}
// ====
// SMTEngine: all
// ----
// Warning 8364: (148-157): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (147-158): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (148-157): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (147-158): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (116-125): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (115-126): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (116-125): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (115-126): Assertion checker does not yet implement type type(uint256[] memory)

79
test/libsolidity/smtCheckerTests/abi/abi_decode_array.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
pragma abicoder v2;
contract C {
@ -29,42 +28,44 @@ contract C {
assert(l.length == b.length); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 8364: (194-200): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (202-208): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (315-321): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (323-329): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (564-570): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (572-578): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (580-586): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (801-807): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (801-809): Assertion checker does not yet implement type type(uint256[] memory[] memory)
// Warning 8364: (811-817): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (811-819): Assertion checker does not yet implement type type(uint256[] memory[] memory)
// Warning 8364: (811-821): Assertion checker does not yet implement type type(uint256[] memory[] memory[] memory)
// Warning 8364: (1021-1027): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (1029-1035): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 6328: (214-242): CHC: Assertion violation happens here.
// Warning 6328: (367-395): CHC: Assertion violation happens here.
// Warning 6328: (446-474): CHC: Assertion violation happens here.
// Warning 6328: (592-620): CHC: Assertion violation happens here.
// Warning 6328: (639-667): CHC: Assertion violation happens here.
// Warning 6328: (686-714): CHC: Assertion violation happens here.
// Warning 6328: (911-948): CHC: Assertion violation happens here.
// Warning 6328: (1041-1069): CHC: Assertion violation happens here.
// Warning 6328: (1088-1116): CHC: Assertion violation happens here.
// Warning 6328: (1135-1163): CHC: Assertion violation happens here.
// Warning 8364: (194-200): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (202-208): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (315-321): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (323-329): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (564-570): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (572-578): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (580-586): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (801-807): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (801-809): Assertion checker does not yet implement type type(uint256[] memory[] memory)
// Warning 8364: (811-817): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (811-819): Assertion checker does not yet implement type type(uint256[] memory[] memory)
// Warning 8364: (811-821): Assertion checker does not yet implement type type(uint256[] memory[] memory[] memory)
// Warning 8364: (1021-1027): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (1029-1035): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (162-168): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (170-176): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (283-289): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (291-297): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (532-538): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (540-546): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (548-554): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (769-775): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (769-777): Assertion checker does not yet implement type type(uint256[] memory[] memory)
// Warning 8364: (779-785): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (779-787): Assertion checker does not yet implement type type(uint256[] memory[] memory)
// Warning 8364: (779-789): Assertion checker does not yet implement type type(uint256[] memory[] memory[] memory)
// Warning 8364: (989-995): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (997-1003): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 6328: (182-210): CHC: Assertion violation happens here.
// Warning 6328: (335-363): CHC: Assertion violation happens here.
// Warning 6328: (414-442): CHC: Assertion violation happens here.
// Warning 6328: (560-588): CHC: Assertion violation happens here.
// Warning 6328: (607-635): CHC: Assertion violation happens here.
// Warning 6328: (654-682): CHC: Assertion violation happens here.
// Warning 6328: (879-916): CHC: Assertion violation happens here.
// Warning 6328: (1009-1037): CHC: Assertion violation happens here.
// Warning 6328: (1056-1084): CHC: Assertion violation happens here.
// Warning 6328: (1103-1131): CHC: Assertion violation happens here.
// Warning 8364: (162-168): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (170-176): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (283-289): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (291-297): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (532-538): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (540-546): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (548-554): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (769-775): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (769-777): Assertion checker does not yet implement type type(uint256[] memory[] memory)
// Warning 8364: (779-785): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (779-787): Assertion checker does not yet implement type type(uint256[] memory[] memory)
// Warning 8364: (779-789): Assertion checker does not yet implement type type(uint256[] memory[] memory[] memory)
// Warning 8364: (989-995): Assertion checker does not yet implement type type(uint256[] memory)
// Warning 8364: (997-1003): Assertion checker does not yet implement type type(uint256[] memory)

16
test/libsolidity/smtCheckerTests/abi/abi_decode_simple.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
function abiDecodeSimple(bytes memory b1, bytes memory b2) public pure {
(uint x, uint y) = abi.decode(b1, (uint, uint));
@ -19,12 +18,13 @@ contract C {
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (241-255): CHC: Assertion violation happens here.
// Warning 6328: (292-306): CHC: Assertion violation happens here.
// Warning 6328: (391-405): CHC: Assertion violation happens here.
// Warning 6328: (424-438): CHC: Assertion violation happens here.
// Warning 6328: (457-466): CHC: Assertion violation happens here.
// Warning 6328: (537-551): CHC: Assertion violation happens here.
// Warning 6328: (570-584): CHC: Assertion violation happens here.
// Warning 6328: (209-223): CHC: Assertion violation happens here.
// Warning 6328: (260-274): CHC: Assertion violation happens here.
// Warning 6328: (359-373): CHC: Assertion violation happens here.
// Warning 6328: (392-406): CHC: Assertion violation happens here.
// Warning 6328: (425-434): CHC: Assertion violation happens here.
// Warning 6328: (505-519): CHC: Assertion violation happens here.
// Warning 6328: (538-552): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/abi/abi_encode_array_slice.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeSlice(bytes calldata data) external pure {
bytes memory b1 = abi.encode(data);
@ -24,6 +23,7 @@ contract C {
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (311-341): CHC: Assertion violation happens here.
// Warning 6328: (279-309): CHC: Assertion violation happens here.

10
test/libsolidity/smtCheckerTests/abi/abi_encode_array_slice_2.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeSlice(uint[] calldata data) external pure {
bytes memory b1 = abi.encode(data);
@ -24,9 +23,10 @@ contract C {
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 2072: (364-379): Unused local variable.
// Warning 2072: (650-665): Unused local variable.
// Warning 2072: (823-838): Unused local variable.
// Warning 6328: (312-342): CHC: Assertion violation happens here.
// Warning 2072: (332-347): Unused local variable.
// Warning 2072: (618-633): Unused local variable.
// Warning 2072: (791-806): Unused local variable.
// Warning 6328: (280-310): CHC: Assertion violation happens here.

7
test/libsolidity/smtCheckerTests/abi/abi_encode_function.sol
View File

@ -1,9 +1,10 @@
pragma experimental SMTChecker;
contract C {
function f() public view {
abi.encode(this.f);
}
}
// ====
// SMTEngine: all
// ----
// Warning 6031: (86-92): Internal error: Expression undefined for SMT solver.
// Warning 6031: (86-92): Internal error: Expression undefined for SMT solver.
// Warning 6031: (54-60): Internal error: Expression undefined for SMT solver.
// Warning 6031: (54-60): Internal error: Expression undefined for SMT solver.

3
test/libsolidity/smtCheckerTests/abi/abi_encode_hash.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeHash(uint a, uint b) public pure {
require(a == b);
@ -7,3 +6,5 @@ contract C {
assert(keccak256(b1) == keccak256(b2));
}
}
// ====
// SMTEngine: all

10
test/libsolidity/smtCheckerTests/abi/abi_encode_no_arguments.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
function f() pure public {
bytes memory res = abi.encode();
@ -14,9 +13,10 @@ contract C {
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (152-174): CHC: Assertion violation happens here.
// Warning 6328: (263-285): CHC: Assertion violation happens here.
// Warning 6328: (339-362): CHC: Assertion violation happens here.
// Warning 6328: (455-478): CHC: Assertion violation happens here.
// Warning 6328: (120-142): CHC: Assertion violation happens here.
// Warning 6328: (231-253): CHC: Assertion violation happens here.
// Warning 6328: (307-330): CHC: Assertion violation happens here.
// Warning 6328: (423-446): CHC: Assertion violation happens here.

10
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_array_slice.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
function abiencodePackedSlice(bytes calldata data) external pure {
bytes memory b1 = abi.encodePacked(data);
@ -28,9 +27,10 @@ contract C {
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 2072: (159-174): Unused local variable.
// Warning 2072: (723-738): Unused local variable.
// Warning 2072: (1131-1146): Unused local variable.
// Warning 6328: (1079-1109): CHC: Assertion violation happens here.
// Warning 2072: (127-142): Unused local variable.
// Warning 2072: (691-706): Unused local variable.
// Warning 2072: (1099-1114): Unused local variable.
// Warning 6328: (1047-1077): CHC: Assertion violation happens here.

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

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
function abiencodePackedSlice(uint[] calldata data) external pure {
bytes memory b1 = abi.encodePacked(data);
@ -27,6 +26,8 @@ contract C {
//assert(b4.length == b6.length); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 2072: (675-690): Unused local variable.
// Warning 6328: (330-360): CHC: Assertion violation happens here.
// Warning 2072: (643-658): Unused local variable.
// Warning 6328: (298-328): CHC: Assertion violation happens here.

9
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_hash.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
function abiencodePackedHash(uint a, uint b) public pure {
require(a == b);
@ -10,7 +9,9 @@ contract C {
assert(keccak256(b1) == keccak256(b3)); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 1218: (313-351): CHC: Error trying to invoke SMT solver.
// Warning 6328: (313-351): CHC: Assertion violation might happen here.
// Warning 4661: (313-351): BMC: Assertion violation happens here.
// Warning 1218: (281-319): CHC: Error trying to invoke SMT solver.
// Warning 6328: (281-319): CHC: Assertion violation might happen here.
// Warning 4661: (281-319): BMC: Assertion violation happens here.

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

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
function abiencodePackedSimple(bool t, uint x, uint y, uint z, uint[] memory a, uint[] memory b) public pure {
require(x == y);
@ -21,8 +20,10 @@ contract C {
//assert(b1.length == b6.length); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (354-384): CHC: Assertion violation happens here.
// Warning 6328: (451-481): CHC: Assertion violation happens here.
// Warning 6328: (560-590): CHC: Assertion violation happens here.
// Warning 6328: (609-639): CHC: Assertion violation happens here.
// Warning 6328: (322-352): CHC: Assertion violation happens here.
// Warning 6328: (419-449): CHC: Assertion violation happens here.
// Warning 6328: (528-558): CHC: Assertion violation happens here.
// Warning 6328: (577-607): CHC: Assertion violation happens here.

29
test/libsolidity/smtCheckerTests/abi/abi_encode_packed_string_literal.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
function abiencodePackedStringLiteral() public pure {
bytes memory b1 = abi.encodePacked("");
@ -20,17 +19,19 @@ contract C {
assert(b1.length == b6.length); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (258-288): CHC: Assertion violation happens here.
// Warning 1218: (342-372): CHC: Error trying to invoke SMT solver.
// Warning 6328: (342-372): CHC: Assertion violation might happen here.
// Warning 1218: (515-545): CHC: Error trying to invoke SMT solver.
// Warning 6328: (515-545): CHC: Assertion violation might happen here.
// Warning 1218: (600-630): CHC: Error trying to invoke SMT solver.
// Warning 6328: (600-630): CHC: Assertion violation might happen here.
// Warning 1218: (686-716): CHC: Error trying to invoke SMT solver.
// Warning 6328: (686-716): CHC: Assertion violation might happen here.
// Warning 4661: (342-372): BMC: Assertion violation happens here.
// Warning 4661: (515-545): BMC: Assertion violation happens here.
// Warning 4661: (600-630): BMC: Assertion violation happens here.
// Warning 4661: (686-716): BMC: Assertion violation happens here.
// Warning 6328: (226-256): CHC: Assertion violation happens here.
// Warning 1218: (310-340): CHC: Error trying to invoke SMT solver.
// Warning 6328: (310-340): CHC: Assertion violation might happen here.
// Warning 1218: (483-513): CHC: Error trying to invoke SMT solver.
// Warning 6328: (483-513): CHC: Assertion violation might happen here.
// Warning 1218: (568-598): CHC: Error trying to invoke SMT solver.
// Warning 6328: (568-598): CHC: Assertion violation might happen here.
// Warning 1218: (654-684): CHC: Error trying to invoke SMT solver.
// Warning 6328: (654-684): CHC: Assertion violation might happen here.
// Warning 4661: (310-340): BMC: Assertion violation happens here.
// Warning 4661: (483-513): BMC: Assertion violation happens here.
// Warning 4661: (568-598): BMC: Assertion violation happens here.
// Warning 4661: (654-684): BMC: Assertion violation happens here.

9
test/libsolidity/smtCheckerTests/abi/abi_encode_simple.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeSimple(bool t, uint x, uint y, uint z, uint[] memory a, uint[] memory b) public pure {
require(x == y);
@ -18,7 +17,9 @@ contract C {
//assert(b1.length == b5.length); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (330-360): CHC: Assertion violation happens here.
// Warning 6328: (421-451): CHC: Assertion violation happens here.
// Warning 6328: (524-554): CHC: Assertion violation happens here.
// Warning 6328: (298-328): CHC: Assertion violation happens here.
// Warning 6328: (389-419): CHC: Assertion violation happens here.
// Warning 6328: (492-522): CHC: Assertion violation happens here.

27
test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeStringLiteral() public pure {
bytes memory b1 = abi.encode("");
@ -17,16 +16,18 @@ contract C {
assert(b1.length == b5.length); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 1218: (240-270): CHC: Error trying to invoke SMT solver.
// Warning 6328: (240-270): CHC: Assertion violation might happen here.
// Warning 1218: (318-348): CHC: Error trying to invoke SMT solver.
// Warning 6328: (318-348): CHC: Assertion violation might happen here.
// Warning 1218: (485-515): CHC: Error trying to invoke SMT solver.
// Warning 6328: (485-515): CHC: Assertion violation might happen here.
// Warning 1218: (564-594): CHC: Error trying to invoke SMT solver.
// Warning 6328: (564-594): CHC: Assertion violation might happen here.
// Warning 4661: (240-270): BMC: Assertion violation happens here.
// Warning 4661: (318-348): BMC: Assertion violation happens here.
// Warning 4661: (485-515): BMC: Assertion violation happens here.
// Warning 4661: (564-594): BMC: Assertion violation happens here.
// Warning 1218: (208-238): CHC: Error trying to invoke SMT solver.
// Warning 6328: (208-238): CHC: Assertion violation might happen here.
// Warning 1218: (286-316): CHC: Error trying to invoke SMT solver.
// Warning 6328: (286-316): CHC: Assertion violation might happen here.
// Warning 1218: (453-483): CHC: Error trying to invoke SMT solver.
// Warning 6328: (453-483): CHC: Assertion violation might happen here.
// Warning 1218: (532-562): CHC: Error trying to invoke SMT solver.
// Warning 6328: (532-562): CHC: Assertion violation might happen here.
// Warning 4661: (208-238): BMC: Assertion violation happens here.
// Warning 4661: (286-316): BMC: Assertion violation happens here.
// Warning 4661: (453-483): BMC: Assertion violation happens here.
// Warning 4661: (532-562): BMC: Assertion violation happens here.

25
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeSlice(bytes4 sel, bytes calldata data) external pure {
bytes memory b1 = abi.encodeWithSelector(sel, data);
@ -23,15 +22,17 @@ contract C {
assert(b4.length == b6.length); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (357-387): CHC: Assertion violation happens here.
// Warning 6328: (610-640): CHC: Assertion violation happens here.
// Warning 1218: (723-753): CHC: Error trying to invoke SMT solver.
// Warning 6328: (723-753): CHC: Assertion violation might happen here.
// Warning 1218: (991-1021): CHC: Error trying to invoke SMT solver.
// Warning 6328: (991-1021): CHC: Assertion violation might happen here.
// Warning 1218: (1111-1141): CHC: Error trying to invoke SMT solver.
// Warning 6328: (1111-1141): CHC: Assertion violation might happen here.
// Warning 4661: (723-753): BMC: Assertion violation happens here.
// Warning 4661: (991-1021): BMC: Assertion violation happens here.
// Warning 4661: (1111-1141): BMC: Assertion violation happens here.
// Warning 6328: (325-355): CHC: Assertion violation happens here.
// Warning 6328: (578-608): CHC: Assertion violation happens here.
// Warning 1218: (691-721): CHC: Error trying to invoke SMT solver.
// Warning 6328: (691-721): CHC: Assertion violation might happen here.
// Warning 1218: (959-989): CHC: Error trying to invoke SMT solver.
// Warning 6328: (959-989): CHC: Assertion violation might happen here.
// Warning 1218: (1079-1109): CHC: Error trying to invoke SMT solver.
// Warning 6328: (1079-1109): CHC: Assertion violation might happen here.
// Warning 4661: (691-721): BMC: Assertion violation happens here.
// Warning 4661: (959-989): BMC: Assertion violation happens here.
// Warning 4661: (1079-1109): BMC: Assertion violation happens here.

25
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_array_slice_2.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeSlice(bytes4 sel, uint[] calldata data) external pure {
bytes memory b1 = abi.encodeWithSelector(sel, data);
@ -23,15 +22,17 @@ contract C {
assert(b4.length == b6.length); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (358-388): CHC: Assertion violation happens here.
// Warning 6328: (611-641): CHC: Assertion violation happens here.
// Warning 1218: (724-754): CHC: Error trying to invoke SMT solver.
// Warning 6328: (724-754): CHC: Assertion violation might happen here.
// Warning 1218: (992-1022): CHC: Error trying to invoke SMT solver.
// Warning 6328: (992-1022): CHC: Assertion violation might happen here.
// Warning 1218: (1112-1142): CHC: Error trying to invoke SMT solver.
// Warning 6328: (1112-1142): CHC: Assertion violation might happen here.
// Warning 4661: (724-754): BMC: Assertion violation happens here.
// Warning 4661: (992-1022): BMC: Assertion violation happens here.
// Warning 4661: (1112-1142): BMC: Assertion violation happens here.
// Warning 6328: (326-356): CHC: Assertion violation happens here.
// Warning 6328: (579-609): CHC: Assertion violation happens here.
// Warning 1218: (692-722): CHC: Error trying to invoke SMT solver.
// Warning 6328: (692-722): CHC: Assertion violation might happen here.
// Warning 1218: (960-990): CHC: Error trying to invoke SMT solver.
// Warning 6328: (960-990): CHC: Assertion violation might happen here.
// Warning 1218: (1080-1110): CHC: Error trying to invoke SMT solver.
// Warning 6328: (1080-1110): CHC: Assertion violation might happen here.
// Warning 4661: (692-722): BMC: Assertion violation happens here.
// Warning 4661: (960-990): BMC: Assertion violation happens here.
// Warning 4661: (1080-1110): BMC: Assertion violation happens here.

15
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeHash(bytes4 sel, uint a, uint b) public pure {
require(a == b);
@ -11,10 +10,12 @@ contract C {
assert(keccak256(b1) != keccak256(b3)); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 1218: (365-403): CHC: Error trying to invoke SMT solver.
// Warning 6328: (365-403): CHC: Assertion violation might happen here.
// Warning 1218: (422-460): CHC: Error trying to invoke SMT solver.
// Warning 6328: (422-460): CHC: Assertion violation might happen here.
// Warning 4661: (365-403): BMC: Assertion violation happens here.
// Warning 4661: (422-460): BMC: Assertion violation happens here.
// Warning 1218: (333-371): CHC: Error trying to invoke SMT solver.
// Warning 6328: (333-371): CHC: Assertion violation might happen here.
// Warning 1218: (390-428): CHC: Error trying to invoke SMT solver.
// Warning 6328: (390-428): CHC: Assertion violation might happen here.
// Warning 4661: (333-371): BMC: Assertion violation happens here.
// Warning 4661: (390-428): BMC: Assertion violation happens here.

13
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_simple.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeSimple(bytes4 sel, bool t, uint x, uint y, uint z, uint[] memory a, uint[] memory b) public pure {
require(x == y);
@ -22,9 +21,11 @@ contract C {
assert(b1.length == b6.length); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 5667: (132-147): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 6328: (603-633): CHC: Assertion violation happens here.
// Warning 6328: (723-753): CHC: Assertion violation happens here.
// Warning 6328: (772-802): CHC: Assertion violation happens here.
// Warning 6328: (887-917): CHC: Assertion violation happens here.
// Warning 5667: (100-115): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 6328: (571-601): CHC: Assertion violation happens here.
// Warning 6328: (691-721): CHC: Assertion violation happens here.
// Warning 6328: (740-770): CHC: Assertion violation happens here.
// Warning 6328: (855-885): CHC: Assertion violation happens here.

29
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_string_literal.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeStringLiteral(bytes4 sel) public pure {
bytes memory b1 = abi.encodeWithSelector(sel, "");
@ -20,17 +19,19 @@ contract C {
assert(b4.length == b6.length); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (284-314): CHC: Assertion violation happens here.
// Warning 1218: (379-409): CHC: Error trying to invoke SMT solver.
// Warning 6328: (379-409): CHC: Assertion violation might happen here.
// Warning 1218: (563-593): CHC: Error trying to invoke SMT solver.
// Warning 6328: (563-593): CHC: Assertion violation might happen here.
// Warning 1218: (659-689): CHC: Error trying to invoke SMT solver.
// Warning 6328: (659-689): CHC: Assertion violation might happen here.
// Warning 1218: (778-808): CHC: Error trying to invoke SMT solver.
// Warning 6328: (778-808): CHC: Assertion violation might happen here.
// Warning 4661: (379-409): BMC: Assertion violation happens here.
// Warning 4661: (563-593): BMC: Assertion violation happens here.
// Warning 4661: (659-689): BMC: Assertion violation happens here.
// Warning 4661: (778-808): BMC: Assertion violation happens here.
// Warning 6328: (252-282): CHC: Assertion violation happens here.
// Warning 1218: (347-377): CHC: Error trying to invoke SMT solver.
// Warning 6328: (347-377): CHC: Assertion violation might happen here.
// Warning 1218: (531-561): CHC: Error trying to invoke SMT solver.
// Warning 6328: (531-561): CHC: Assertion violation might happen here.
// Warning 1218: (627-657): CHC: Error trying to invoke SMT solver.
// Warning 6328: (627-657): CHC: Assertion violation might happen here.
// Warning 1218: (746-776): CHC: Error trying to invoke SMT solver.
// Warning 6328: (746-776): CHC: Assertion violation might happen here.
// Warning 4661: (347-377): BMC: Assertion violation happens here.
// Warning 4661: (531-561): BMC: Assertion violation happens here.
// Warning 4661: (627-657): BMC: Assertion violation happens here.
// Warning 4661: (746-776): BMC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_string_literal_2.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeStringLiteral(bytes4 sel) public pure {
bytes memory b1 = abi.encodeWithSelector("");
@ -7,3 +6,5 @@ contract C {
assert(b1.length == b2.length); // should hold
}
}
// ====
// SMTEngine: all

5
test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_vs_sig.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
function f(string memory sig, uint x, uint[] memory a) public pure {
bytes memory b1 = abi.encodeWithSignature(sig, x, a);
@ -7,5 +6,7 @@ contract C {
assert(b1.length == b2.length);
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (326-356): CHC: Assertion violation happens here.
// Warning 6328: (294-324): CHC: Assertion violation happens here.

25
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeSlice(string memory sig, bytes calldata data) external pure {
bytes memory b1 = abi.encodeWithSignature(sig, data);
@ -23,15 +22,17 @@ contract C {
assert(b4.length == b6.length); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (366-396): CHC: Assertion violation happens here.
// Warning 6328: (620-650): CHC: Assertion violation happens here.
// Warning 1218: (734-764): CHC: Error trying to invoke SMT solver.
// Warning 6328: (734-764): CHC: Assertion violation might happen here.
// Warning 1218: (1003-1033): CHC: Error trying to invoke SMT solver.
// Warning 6328: (1003-1033): CHC: Assertion violation might happen here.
// Warning 1218: (1118-1148): CHC: Error trying to invoke SMT solver.
// Warning 6328: (1118-1148): CHC: Assertion violation might happen here.
// Warning 4661: (734-764): BMC: Assertion violation happens here.
// Warning 4661: (1003-1033): BMC: Assertion violation happens here.
// Warning 4661: (1118-1148): BMC: Assertion violation happens here.
// Warning 6328: (334-364): CHC: Assertion violation happens here.
// Warning 6328: (588-618): CHC: Assertion violation happens here.
// Warning 1218: (702-732): CHC: Error trying to invoke SMT solver.
// Warning 6328: (702-732): CHC: Assertion violation might happen here.
// Warning 1218: (971-1001): CHC: Error trying to invoke SMT solver.
// Warning 6328: (971-1001): CHC: Assertion violation might happen here.
// Warning 1218: (1086-1116): CHC: Error trying to invoke SMT solver.
// Warning 6328: (1086-1116): CHC: Assertion violation might happen here.
// Warning 4661: (702-732): BMC: Assertion violation happens here.
// Warning 4661: (971-1001): BMC: Assertion violation happens here.
// Warning 4661: (1086-1116): BMC: Assertion violation happens here.

25
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_array_slice_2.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeSlice(string memory sig, uint[] calldata data) external pure {
bytes memory b1 = abi.encodeWithSignature(sig, data);
@ -23,15 +22,17 @@ contract C {
assert(b4.length == b6.length); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (367-397): CHC: Assertion violation happens here.
// Warning 6328: (621-651): CHC: Assertion violation happens here.
// Warning 1218: (735-765): CHC: Error trying to invoke SMT solver.
// Warning 6328: (735-765): CHC: Assertion violation might happen here.
// Warning 1218: (1004-1034): CHC: Error trying to invoke SMT solver.
// Warning 6328: (1004-1034): CHC: Assertion violation might happen here.
// Warning 1218: (1119-1149): CHC: Error trying to invoke SMT solver.
// Warning 6328: (1119-1149): CHC: Assertion violation might happen here.
// Warning 4661: (735-765): BMC: Assertion violation happens here.
// Warning 4661: (1004-1034): BMC: Assertion violation happens here.
// Warning 4661: (1119-1149): BMC: Assertion violation happens here.
// Warning 6328: (335-365): CHC: Assertion violation happens here.
// Warning 6328: (589-619): CHC: Assertion violation happens here.
// Warning 1218: (703-733): CHC: Error trying to invoke SMT solver.
// Warning 6328: (703-733): CHC: Assertion violation might happen here.
// Warning 1218: (972-1002): CHC: Error trying to invoke SMT solver.
// Warning 6328: (972-1002): CHC: Assertion violation might happen here.
// Warning 1218: (1087-1117): CHC: Error trying to invoke SMT solver.
// Warning 6328: (1087-1117): CHC: Assertion violation might happen here.
// Warning 4661: (703-733): BMC: Assertion violation happens here.
// Warning 4661: (972-1002): BMC: Assertion violation happens here.
// Warning 4661: (1087-1117): BMC: Assertion violation happens here.

15
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_hash.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeHash(string memory sig, uint a, uint b) public pure {
require(a == b);
@ -11,10 +10,12 @@ contract C {
assert(keccak256(b1) != keccak256(b3)); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 1218: (369-407): CHC: Error trying to invoke SMT solver.
// Warning 6328: (369-407): CHC: Assertion violation might happen here.
// Warning 1218: (426-464): CHC: Error trying to invoke SMT solver.
// Warning 6328: (426-464): CHC: Assertion violation might happen here.
// Warning 4661: (369-407): BMC: Assertion violation happens here.
// Warning 4661: (426-464): BMC: Assertion violation happens here.
// Warning 1218: (337-375): CHC: Error trying to invoke SMT solver.
// Warning 6328: (337-375): CHC: Assertion violation might happen here.
// Warning 1218: (394-432): CHC: Error trying to invoke SMT solver.
// Warning 6328: (394-432): CHC: Assertion violation might happen here.
// Warning 4661: (337-375): BMC: Assertion violation happens here.
// Warning 4661: (394-432): BMC: Assertion violation happens here.

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

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeSimple(string memory sig, bool t, uint x, uint y, uint z, uint[] memory a, uint[] memory b) public pure {
require(x == y);
@ -21,9 +20,11 @@ contract C {
assert(b1.length == b6.length); // should fail
}
}
// ====
// SMTEngine: all
// ----
// 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 6328: (856-886): CHC: Assertion violation happens here.
// Warning 5667: (107-122): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 6328: (543-573): CHC: Assertion violation happens here.
// Warning 6328: (664-694): CHC: Assertion violation happens here.
// Warning 6328: (713-743): CHC: Assertion violation happens here.
// Warning 6328: (824-854): CHC: Assertion violation happens here.

29
test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_string_literal.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
function abiEncodeStringLiteral(string memory sig) public pure {
bytes memory b1 = abi.encodeWithSignature(sig, "");
@ -20,17 +19,19 @@ contract C {
assert(b4.length == b6.length); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (293-323): CHC: Assertion violation happens here.
// Warning 1218: (389-419): CHC: Error trying to invoke SMT solver.
// Warning 6328: (389-419): CHC: Assertion violation might happen here.
// Warning 1218: (574-604): CHC: Error trying to invoke SMT solver.
// Warning 6328: (574-604): CHC: Assertion violation might happen here.
// Warning 1218: (671-701): CHC: Error trying to invoke SMT solver.
// Warning 6328: (671-701): CHC: Assertion violation might happen here.
// Warning 1218: (785-815): CHC: Error trying to invoke SMT solver.
// Warning 6328: (785-815): CHC: Assertion violation might happen here.
// Warning 4661: (389-419): BMC: Assertion violation happens here.
// Warning 4661: (574-604): BMC: Assertion violation happens here.
// Warning 4661: (671-701): BMC: Assertion violation happens here.
// Warning 4661: (785-815): BMC: Assertion violation happens here.
// Warning 6328: (261-291): CHC: Assertion violation happens here.
// Warning 1218: (357-387): CHC: Error trying to invoke SMT solver.
// Warning 6328: (357-387): CHC: Assertion violation might happen here.
// Warning 1218: (542-572): CHC: Error trying to invoke SMT solver.
// Warning 6328: (542-572): CHC: Assertion violation might happen here.
// Warning 1218: (639-669): CHC: Error trying to invoke SMT solver.
// Warning 6328: (639-669): CHC: Assertion violation might happen here.
// Warning 1218: (753-783): CHC: Error trying to invoke SMT solver.
// Warning 6328: (753-783): CHC: Assertion violation might happen here.
// Warning 4661: (357-387): BMC: Assertion violation happens here.
// Warning 4661: (542-572): BMC: Assertion violation happens here.
// Warning 4661: (639-669): BMC: Assertion violation happens here.
// Warning 4661: (753-783): BMC: Assertion violation happens here.

6
test/libsolidity/smtCheckerTests/array_members/array_pop_length_1.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
function f() public {
@ -7,5 +5,7 @@ contract C {
a.push();
}
}
// ====
// SMTEngine: all
// ----
// Warning 2529: (82-89): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 2529: (49-56): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()

6
test/libsolidity/smtCheckerTests/array_members/array_pop_length_2.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
function f() public {
@ -7,5 +5,7 @@ contract C {
a.length;
}
}
// ====
// SMTEngine: all
// ----
// Warning 2529: (82-89): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 2529: (49-56): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()

8
test/libsolidity/smtCheckerTests/array_members/array_pop_length_3.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
function f() public {
@ -7,6 +5,8 @@ contract C {
a.pop();
}
}
// ====
// SMTEngine: all
// ----
// Warning 2529: (82-89): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 2529: (93-100): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 2529: (49-56): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 2529: (60-67): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()

6
test/libsolidity/smtCheckerTests/array_members/array_pop_length_4.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
function f() public {
@ -7,5 +5,7 @@ contract C {
a.pop();
}
}
// ====
// SMTEngine: all
// ----
// Warning 2529: (94-101): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 2529: (61-68): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()

6
test/libsolidity/smtCheckerTests/array_members/array_pop_length_5.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
function g() internal {
@ -10,5 +8,7 @@ contract C {
g();
}
}
// ====
// SMTEngine: all
// ----
// Warning 2529: (122-129): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 2529: (89-96): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()

6
test/libsolidity/smtCheckerTests/array_members/array_pop_length_6.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
function g() internal view {
@ -10,5 +8,7 @@ contract C {
g();
}
}
// ====
// SMTEngine: all
// ----
// Warning 2529: (127-134): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 2529: (94-101): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()

4
test/libsolidity/smtCheckerTests/array_members/array_pop_length_7.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
function f() public {
@ -7,3 +5,5 @@ contract C {
a.pop();
}
}
// ====
// SMTEngine: all

6
test/libsolidity/smtCheckerTests/array_members/array_pop_length_8.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
function f() public {
@ -12,5 +10,7 @@ contract C {
a.pop();
}
}
// ====
// SMTEngine: all
// ----
// Warning 2529: (82-89): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 2529: (49-56): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()

7
test/libsolidity/smtCheckerTests/array_members/array_push_string_literal.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
bytes data;
function g() public {
@ -12,6 +11,8 @@ contract C {
assert(uint8(data[0]) == 0); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (171-193): CHC: Assertion violation happens here.\nCounterexample:\ndata = [98]\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.g()
// Warning 6328: (295-322): CHC: Assertion violation happens here.\nCounterexample:\ndata = [1]\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.g()
// Warning 6328: (139-161): CHC: Assertion violation happens here.\nCounterexample:\ndata = [98]\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.g()
// Warning 6328: (263-290): CHC: Assertion violation happens here.\nCounterexample:\ndata = [1]\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.g()

3
test/libsolidity/smtCheckerTests/array_members/length_1d_assignment_2d_memory_to_memory.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
pragma abicoder v2;
contract C {
@ -9,3 +8,5 @@ contract C {
assert(arr.length == arr2.length);
}
}
// ====
// SMTEngine: all

3
test/libsolidity/smtCheckerTests/array_members/length_1d_assignment_2d_storage_to_storage.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
pragma abicoder v2;
contract C {
@ -15,3 +14,5 @@ contract C {
assert(arr2.length == arr.length);
}
}
// ====
// SMTEngine: all

3
test/libsolidity/smtCheckerTests/array_members/length_1d_copy_2d_memory_to_storage.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
pragma abicoder v2;
contract C {
@ -10,3 +9,5 @@ contract C {
assert(arr2.length == arr.length);
}
}
// ====
// SMTEngine: all

3
test/libsolidity/smtCheckerTests/array_members/length_1d_copy_2d_storage_to_memory.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
pragma abicoder v2;
contract C {
@ -15,3 +14,5 @@ contract C {
assert(arr2.length == arr.length);
}
}
// ====
// SMTEngine: all

4
test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_1.sol
View File

@ -1,8 +1,8 @@
pragma experimental SMTChecker;
contract C {
mapping (uint => uint[]) map;
function f() public view {
assert(map[0].length == map[1].length);
}
}
// ====
// SMTEngine: all

4
test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_2.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
mapping (uint => uint[]) map;
function f(uint x, uint y) public view {
@ -7,3 +5,5 @@ contract C {
assert(map[x].length == map[y].length);
}
}
// ====
// SMTEngine: all

4
test/libsolidity/smtCheckerTests/array_members/length_1d_mapping_array_2d_1.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
mapping (uint => uint[][]) map;
function f(uint x, uint y) public {
@ -8,3 +6,5 @@ contract C {
assert(map[x][0].length == map[y][0].length);
}
}
// ====
// SMTEngine: all

4
test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_1.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
struct S {
uint[] arr;
@ -10,4 +8,6 @@ contract C {
assert(s1.arr.length == s2.arr.length);
}
}
// ====
// SMTEngine: all
// ----

4
test/libsolidity/smtCheckerTests/array_members/length_1d_struct_array_2d_1.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
struct S {
uint[][] arr;
@ -20,3 +18,5 @@ contract C {
assert(s1.arr[0].length == s2.arr[0].length);
}
}
// ====
// SMTEngine: all

3
test/libsolidity/smtCheckerTests/array_members/length_assignment_2d_memory_to_memory.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
pragma abicoder v2;
contract C {
@ -7,3 +6,5 @@ contract C {
assert(arr2.length == arr.length);
}
}
// ====
// SMTEngine: all

4
test/libsolidity/smtCheckerTests/array_members/length_assignment_memory_to_memory.sol
View File

@ -1,8 +1,8 @@
pragma experimental SMTChecker;
contract C {
function f(uint[] memory arr) public pure {
uint[] memory arr2 = arr;
assert(arr2.length == arr.length);
}
}
// ====
// SMTEngine: all

4
test/libsolidity/smtCheckerTests/array_members/length_assignment_storage_to_storage.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[] arr;
uint[] arr2;
@ -8,3 +6,5 @@ contract C {
assert(arr2.length == arr.length);
}
}
// ====
// SMTEngine: all

6
test/libsolidity/smtCheckerTests/array_members/length_basic.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[] arr;
function f() public view {
@ -9,5 +7,7 @@ contract C {
assert(arr.length != y);
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (153-176): CHC: Assertion violation happens here.\nCounterexample:\narr = []\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: arr = []\nC.f()
// Warning 6328: (120-143): CHC: Assertion violation happens here.\nCounterexample:\narr = []\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: arr = []\nC.f()

4
test/libsolidity/smtCheckerTests/array_members/length_copy_memory_to_storage.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[] arr;
function f(uint[] memory marr) public {
@ -7,3 +5,5 @@ contract C {
assert(marr.length == arr.length);
}
}
// ====
// SMTEngine: all

4
test/libsolidity/smtCheckerTests/array_members/length_copy_storage_to_memory.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[] arr;
function f() public view {
@ -7,3 +5,5 @@ contract C {
assert(marr.length == arr.length);
}
}
// ====
// SMTEngine: all

4
test/libsolidity/smtCheckerTests/array_members/length_function_call.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[] arr;
function f() public view {
@ -8,3 +6,5 @@ contract C {
function g() internal pure returns (uint[] memory) {
}
}
// ====
// SMTEngine: all

4
test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[] arr;
constructor() {
@ -14,3 +12,5 @@ contract C {
assert(arr.length == arr2.length);
}
}
// ====
// SMTEngine: all

4
test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[][] arr;
constructor() {
@ -22,3 +20,5 @@ contract C {
assert(arr.length == z);
}
}
// ====
// SMTEngine: all

9
test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_2_fail.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[][] arr;
constructor() {
@ -23,8 +21,9 @@ contract C {
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (324-350): CHC: Assertion violation happens here.
// Warning 6328: (354-380): CHC: Assertion violation happens here.
// Warning 6328: (384-407): CHC: Assertion violation happens here.
// Warning 6328: (291-317): CHC: Assertion violation happens here.
// Warning 6328: (321-347): CHC: Assertion violation happens here.
// Warning 6328: (351-374): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[][] arr;
@ -27,3 +25,5 @@ contract C {
assert(arr[5].length == t);
}
}
// ====
// SMTEngine: all

12
test/libsolidity/smtCheckerTests/array_members/length_same_after_assignment_3_fail.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[][] arr;
constructor() {
@ -25,8 +23,10 @@ contract C {
assert(arr[5].length != t);
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (352-378): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()
// Warning 6328: (382-408): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()
// Warning 6328: (412-435): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()
// Warning 6328: (439-465): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()
// Warning 6328: (319-345): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()
// Warning 6328: (349-375): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()
// Warning 6328: (379-402): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()
// Warning 6328: (406-432): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()

4
test/libsolidity/smtCheckerTests/array_members/pop_1_safe.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
function f() public {
@ -7,3 +5,5 @@ contract C {
a.pop();
}
}
// ====
// SMTEngine: all

6
test/libsolidity/smtCheckerTests/array_members/pop_1_unsafe.sol
View File

@ -1,10 +1,10 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
function f() public {
a.pop();
}
}
// ====
// SMTEngine: all
// ----
// Warning 2529: (82-89): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 2529: (49-56): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()

4
test/libsolidity/smtCheckerTests/array_members/pop_2d_safe.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[][] a;
function f() public {
@ -8,3 +6,5 @@ contract C {
a[0].pop();
}
}
// ====
// SMTEngine: all

6
test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[][] a;
function f() public {
@ -9,5 +7,7 @@ contract C {
a[1].pop();
}
}
// ====
// SMTEngine: all
// ----
// Warning 2529: (123-133): CHC: Empty array "pop" happens here.\nCounterexample:\na = [[0], []]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 2529: (90-100): CHC: Empty array "pop" happens here.\nCounterexample:\na = [[0], []]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()

4
test/libsolidity/smtCheckerTests/array_members/pop_constructor_safe.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
constructor() {
@ -7,3 +5,5 @@ contract C {
a.pop();
}
}
// ====
// SMTEngine: all

6
test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol
View File

@ -1,10 +1,10 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
constructor() {
a.pop();
}
}
// ====
// SMTEngine: all
// ----
// Warning 2529: (76-83): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()
// Warning 2529: (43-50): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()

4
test/libsolidity/smtCheckerTests/array_members/pop_loop_safe.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
function f(uint l) public {
@ -9,4 +7,6 @@ contract C {
}
}
}
// ====
// SMTEngine: all
// ----

6
test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
function f(uint l) public {
@ -10,5 +8,7 @@ contract C {
a.pop();
}
}
// ====
// SMTEngine: all
// ----
// Warning 2529: (150-157): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\nl = 0\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f(0)
// Warning 2529: (117-124): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\nl = 0\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f(0)

4
test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_safe.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[][] a;
function f(uint[] memory x, uint y) public {
@ -8,3 +6,5 @@ contract C {
assert(a[0][a[0].length - 1] == y);
}
}
// ====
// SMTEngine: all

7
test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[][] a;
function f(uint[] memory x, uint y) public {
@ -10,7 +8,8 @@ contract C {
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 3944: (162-177): CHC: Underflow (resulting value less than 0) happens here.
// Warning 6328: (150-184): CHC: Assertion violation happens here.
// Warning 3944: (129-144): CHC: Underflow (resulting value less than 0) happens here.
// Warning 6328: (117-151): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/array_members/push_arg_1.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
function f(uint x) public {
@ -7,3 +5,5 @@ contract C {
assert(a[a.length - 1] == x);
}
}
// ====
// SMTEngine: all

6
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[] b;
@ -17,5 +15,7 @@ contract C {
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (232-262): CHC: Assertion violation happens here.\nCounterexample:\nb = [1]\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.g()
// Warning 6328: (199-229): CHC: Assertion violation happens here.\nCounterexample:\nb = [1]\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.g()

6
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_2d.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[][] c;
@ -20,5 +18,7 @@ contract C {
assert(c[c.length - 1][c[c.length - 1].length - 1] == 200);
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (395-453): CHC: Assertion violation happens here.\nCounterexample:\nc = [[2]]\n\nTransaction trace:\nC.constructor()\nState: c = []\nC.g()
// Warning 6328: (362-420): CHC: Assertion violation happens here.\nCounterexample:\nc = [[2]]\n\nTransaction trace:\nC.constructor()\nState: c = []\nC.g()

3
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_2d_2.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
int[][] array2d;
function s() public returns (int[] memory) {
@ -7,3 +6,5 @@ contract C {
return array2d[1];
}
}
// ====
// SMTEngine: all

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

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[][][] c;
@ -26,6 +24,7 @@ contract C {
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (570-625): CHC: Assertion violation happens here.
// Warning 6328: (537-592): CHC: Assertion violation happens here.

6
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_1d.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[] b;
function f() public {
@ -12,5 +10,7 @@ contract C {
assert(b[length - 1] == 1);
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (237-263): CHC: Assertion violation happens here.\nCounterexample:\nb = [0, 0]\nlength = 2\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.f()
// Warning 6328: (204-230): CHC: Assertion violation happens here.\nCounterexample:\nb = [0, 0]\nlength = 2\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.f()

6
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_2d_1.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[][] b;
function f() public {
@ -15,5 +13,7 @@ contract C {
assert(b[0][0] != b[1][0]);
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (317-343): CHC: Assertion violation happens here.\nCounterexample:\nb = [[0], [0]]\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.f()
// Warning 6328: (284-310): CHC: Assertion violation happens here.\nCounterexample:\nb = [[0], [0]]\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.f()

4
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_2d_2.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[][] b;
function f() public {
@ -13,3 +11,5 @@ contract C {
assert(b[length - 1][length1 - 1] == 0);
}
}
// ====
// SMTEngine: all

6
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_bytes.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
bytes b;
function f() public {
@ -12,5 +10,7 @@ contract C {
assert(b[length - 1] == bytes1(uint8(1)));
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (236-277): CHC: Assertion violation happens here.\nCounterexample:\nb = [0, 0]\nlength = 2\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.f()
// Warning 6328: (203-244): CHC: Assertion violation happens here.\nCounterexample:\nb = [0, 0]\nlength = 2\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.f()

6
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
bytes b;
@ -18,5 +16,7 @@ contract C {
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (298-343): CHC: Assertion violation happens here.\nCounterexample:\nb = [1]\none = 1\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.g()
// Warning 6328: (265-310): CHC: Assertion violation happens here.\nCounterexample:\nb = [1]\none = 1\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.g()

6
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes_2d.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
bytes[] c;
@ -22,5 +20,7 @@ contract C {
assert(c[c.length - 1][c[c.length - 1].length - 1] == bytes1(uint8(100)));
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (468-541): CHC: Assertion violation happens here.\nCounterexample:\nc = [[2]]\nval = 2\n\nTransaction trace:\nC.constructor()\nState: c = []\nC.g()
// Warning 6328: (435-508): CHC: Assertion violation happens here.\nCounterexample:\nc = [[2]]\nval = 2\n\nTransaction trace:\nC.constructor()\nState: c = []\nC.g()

6
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_compound_assignment.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
int[] u;
@ -11,5 +9,7 @@ contract C {
assert(u[0] >= 0); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (161-178): CHC: Assertion violation happens here.\nCounterexample:\nu = [(- 1)]\n\nTransaction trace:\nC.constructor()\nState: u = []\nC.t()
// Warning 6328: (128-145): CHC: Assertion violation happens here.\nCounterexample:\nu = [(- 1)]\n\nTransaction trace:\nC.constructor()\nState: u = []\nC.t()

3
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_struct.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
struct S {
int[] b;
@ -13,3 +12,5 @@ contract C {
assert(s.b[s.b.length -1] == t.s.b[t.s.b.length - 1]);
}
}
// ====
// SMTEngine: all

4
test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint256[] x;
constructor() { x.push(42); }
@ -8,3 +6,5 @@ contract C {
assert(x[0] == 42 || x[0] == 23);
}
}
// ====
// SMTEngine: all

4
test/libsolidity/smtCheckerTests/array_members/push_overflow_1_safe_no_overflow_assumption.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint256[] x;
constructor() { x.push(42); }
@ -8,3 +6,5 @@ contract C {
assert(x[0] == 42);
}
}
// ====
// SMTEngine: all

2
test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe.sol
View File

@ -10,3 +10,5 @@ contract C {
}
}
// ====
// SMTEngine: all

4
test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint256[] x;
function f(uint256 l) public {
@ -11,4 +9,6 @@ contract C {
assert(x[0] == 42);
}
}
// ====
// SMTEngine: all
// ----

3
test/libsolidity/smtCheckerTests/array_members/push_push_no_args_1.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
int[][] array2d;
function l() public {
@ -7,3 +6,5 @@ contract C {
assert(array2d[array2d.length - 1].length > 0);
}
}
// ====
// SMTEngine: all

7
test/libsolidity/smtCheckerTests/array_members/push_push_no_args_1_fail.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
int[][] array2d;
function l() public {
@ -7,6 +6,8 @@ contract C {
assert(array2d[array2d.length - 1].length > 3);
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (113-139): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[0]]\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()
// Warning 6328: (143-189): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[0]]\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()
// Warning 6328: (81-107): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[0]]\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()
// Warning 6328: (111-157): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[0]]\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()

3
test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
int[][][] array2d;
function l() public {
@ -9,3 +8,5 @@ contract C {
assert(array2d[array2d.length - 1][last - 1].length > 0);
}
}
// ====
// SMTEngine: all

9
test/libsolidity/smtCheckerTests/array_members/push_push_no_args_2_fail.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
int[][][] array2d;
function l() public {
@ -9,7 +8,9 @@ contract C {
assert(array2d[array2d.length - 1][last - 1].length > 4);
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (122-148): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[[0]]]\nlast = 0\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()
// Warning 6328: (202-218): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[[0]]]\nlast = 1\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()
// Warning 6328: (222-278): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[[0]]]\nlast = 1\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()
// Warning 6328: (90-116): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[[0]]]\nlast = 0\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()
// Warning 6328: (170-186): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[[0]]]\nlast = 1\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()
// Warning 6328: (190-246): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[[0]]]\nlast = 1\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()

11
test/libsolidity/smtCheckerTests/array_members/push_storage_ref_safe_aliasing.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[][] a;
function f() public {
@ -12,9 +10,10 @@ contract C {
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6368: (212-216): CHC: Out of bounds access happens here.
// Warning 6368: (217-221): CHC: Out of bounds access happens here.
// Warning 3944: (217-232): CHC: Underflow (resulting value less than 0) happens here.
// Warning 6328: (205-239): CHC: Assertion violation happens here.
// Warning 6368: (179-183): CHC: Out of bounds access happens here.
// Warning 6368: (184-188): CHC: Out of bounds access happens here.
// Warning 3944: (184-199): CHC: Underflow (resulting value less than 0) happens here.
// Warning 6328: (172-206): CHC: Assertion violation happens here.

10
test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[][] a;
function f() public {
@ -12,7 +10,9 @@ contract C {
assert(a[0][0] == 16);
}
}
// ====
// SMTEngine: all
// ----
// Warning 6368: (221-225): CHC: Out of bounds access happens here.\nCounterexample:\na = []\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 6368: (221-228): CHC: Out of bounds access happens here.\nCounterexample:\na = [[], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15]]\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 6328: (214-235): CHC: Assertion violation happens here.\nCounterexample:\n\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 6368: (188-192): CHC: Out of bounds access happens here.\nCounterexample:\na = []\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 6368: (188-195): CHC: Out of bounds access happens here.\nCounterexample:\na = [[], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15]]\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 6328: (181-202): CHC: Assertion violation happens here.\nCounterexample:\n\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()

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

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[][] a;
uint[][][] c;
@ -25,14 +23,16 @@ contract C {
//assert(d[1] == 7);
}
}
// ====
// SMTEngine: all
// ----
// Warning 6368: (271-275): CHC: Out of bounds access happens here.
// Warning 6368: (271-278): CHC: Out of bounds access might happen here.
// Warning 6368: (271-281): CHC: Out of bounds access might happen here.
// Warning 6368: (344-348): CHC: Out of bounds access happens here.
// Warning 6368: (376-380): CHC: Out of bounds access happens here.
// Warning 6328: (369-393): CHC: Assertion violation happens here.
// Warning 6368: (546-550): CHC: Out of bounds access happens here.
// Warning 6368: (546-553): CHC: Out of bounds access happens here.
// Warning 6368: (546-556): CHC: Out of bounds access happens here.
// Warning 6328: (539-563): CHC: Assertion violation happens here.
// Warning 6368: (238-242): CHC: Out of bounds access happens here.
// Warning 6368: (238-245): CHC: Out of bounds access might happen here.
// Warning 6368: (238-248): CHC: Out of bounds access might happen here.
// Warning 6368: (311-315): CHC: Out of bounds access happens here.
// Warning 6368: (343-347): CHC: Out of bounds access happens here.
// Warning 6328: (336-360): CHC: Assertion violation happens here.
// Warning 6368: (513-517): CHC: Out of bounds access happens here.
// 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.

3
test/libsolidity/smtCheckerTests/array_members/push_struct_member_1.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
struct S {
int[] b;
@ -14,4 +13,6 @@ contract C {
}
}
// ====
// SMTEngine: all
// ----

3
test/libsolidity/smtCheckerTests/array_members/push_struct_member_2.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
struct S {
int[] b;
@ -15,4 +14,6 @@ contract C {
}
}
// ====
// SMTEngine: all
// ----

4
test/libsolidity/smtCheckerTests/array_members/push_zero_2d_safe.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[][] a;
function f() public {
@ -8,3 +6,5 @@ contract C {
assert(a[a.length - 1][0] == 0);
}
}
// ====
// SMTEngine: all

6
test/libsolidity/smtCheckerTests/array_members/push_zero_2d_unsafe.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[][] a;
function f() public {
@ -8,5 +6,7 @@ contract C {
assert(a[a.length - 1][0] == 100);
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (122-155): CHC: Assertion violation happens here.\nCounterexample:\na = [[0]]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 6328: (89-122): CHC: Assertion violation happens here.\nCounterexample:\na = [[0]]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()

4
test/libsolidity/smtCheckerTests/array_members/push_zero_safe.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
function f() public {
@ -7,3 +5,5 @@ contract C {
assert(a[a.length - 1] == 0);
}
}
// ====
// SMTEngine: all

6
test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol
View File

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint[] a;
function f() public {
@ -7,5 +5,7 @@ contract C {
assert(a[a.length - 1] == 100);
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (94-124): CHC: Assertion violation happens here.\nCounterexample:\na = [0]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Warning 6328: (61-91): CHC: Assertion violation happens here.\nCounterexample:\na = [0]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()

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

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
int[][] array2d;
function l() public {
@ -14,5 +13,7 @@ contract C {
return array2d[2];
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (184-213): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[], [], []]\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()\n C.s() -- internal call
// Warning 6328: (152-181): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[], [], []]\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.l()\n C.s() -- internal call

3
test/libsolidity/smtCheckerTests/array_members/storage_pointer_push_1_safe.sol
View File

@ -1,4 +1,3 @@
pragma experimental SMTChecker;
contract C {
int[][] array2d;
function l() public {
@ -13,3 +12,5 @@ contract C {
return array2d[2];
}
}
// ====
// SMTEngine: all

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

@ -1,5 +1,3 @@
pragma experimental SMTChecker;
contract C {
uint t;
constructor() {
@ -17,4 +15,6 @@ contract C {
//assert(address(this).balance == t);
}
}
// ====
// SMTEngine: all
// ----

Some files were not shown because too many files have changed in this diff Show More