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

Adjust tests for nondeterminism

Browse Source
This commit is contained in:
Leo Alt 2021-08-23 11:30:12 +02:00
parent facc66997b
commit a9af63187e
31 changed files with 81 additions and 80 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -30,6 +30,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// 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)

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

@ -24,6 +24,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 1218: (578-608): CHC: Error trying to invoke SMT solver.
// Warning 1218: (691-721): CHC: Error trying to invoke SMT solver.

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

@ -23,11 +23,12 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 5667: (100-115): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 1218: (855-885): CHC: Error trying to invoke SMT solver.
// Warning 6328: (571-601): CHC: Assertion violation happens here.\nCounterexample:\n\nsel = 0\nt = false\nx = 0\ny = 0\nz = 0\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeSimple(0, false, 0, 0, 0, a, b)
// 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.\nCounterexample:\n\nsel = 0\nt = false\nx = 0\ny = 0\nz = 0\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeSimple(0, false, 0, 0, 0, a, b)
// Warning 6328: (740-770): CHC: Assertion violation happens here.
// Warning 6328: (855-885): CHC: Assertion violation might happen here.
// Warning 4661: (855-885): BMC: Assertion violation happens here.

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

@ -15,5 +15,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// 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
// Warning 6328: (152-181): CHC: Assertion violation happens here.

5
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive.sol
View File

@ -12,6 +12,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (132-188): CHC: Assertion violation happens here.\nCounterexample:\nprevBalance = 0\n\nTransaction trace:\nC.constructor()\nState: prevBalance = 0\nC.f(){ value: 168 }
// Warning 6328: (269-324): CHC: Assertion violation happens here.\nCounterexample:\nprevBalance = 0\n\nTransaction trace:\nC.constructor()\nState: prevBalance = 0\nC.f(){ value: 1201 }
// Warning 6328: (132-188): CHC: Assertion violation happens here.
// Warning 6328: (269-324): CHC: Assertion violation happens here.

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

@ -5,7 +5,7 @@ contract C {
++c;
}
function inv() public view {
assert(address(this).balance >= c * 10); // should hold
assert(address(this).balance >= c * 11); // should hold
assert(address(this).balance >= c * 12); // should fail
}
}

1
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls.sol
View File

@ -15,3 +15,4 @@ contract C {
// ----
// Warning 1218: (131-165): CHC: Error trying to invoke SMT solver.
// Warning 6328: (131-165): CHC: Assertion violation might happen here.
// Warning 4661: (131-165): BMC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_2.sol
View File

@ -8,6 +8,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 9302: (82-93): Return value of low-level calls not used.
// Warning 6328: (97-131): CHC: Assertion violation happens here.\nCounterexample:\n\n_a = 0\nx = 5921\n\nTransaction trace:\nC.constructor()\nC.f(0)\n _a.call("") -- untrusted external call, synthesized as:\n C.f(0) -- reentrant call\n _a.call("") -- untrusted external call
// Warning 6328: (97-131): CHC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_mutex.sol
View File

@ -19,5 +19,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (277-310): CHC: Assertion violation happens here.\nCounterexample:\nlock = true\n_i = 0\nx = 730\n\nTransaction trace:\nC.constructor()\nState: lock = false\nC.f(0)\n _i.ext() -- untrusted external call
// Warning 6328: (277-310): CHC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/blockchain_state/balance_spend.sol
View File

@ -16,6 +16,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (280-314): CHC: Assertion violation happens here.\nCounterexample:\nc = 2\n\nTransaction trace:\nC.constructor(){ value: 101 }\nState: c = 0\nC.f(15, 6)\nState: c = 1\nC.f(5599, 8)\nState: c = 2\nC.inv()
// Warning 6328: (280-314): CHC: Assertion violation happens here.
// Warning 1236: (175-190): BMC: Insufficient funds happens here.

5
test/libsolidity/smtCheckerTests/blockchain_state/balance_spend_2.sol
View File

@ -14,10 +14,11 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 1218: (193-226): CHC: Error trying to invoke SMT solver.
// Warning 6328: (193-226): CHC: Assertion violation might happen here.
// Warning 6328: (245-279): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor(){ value: 101 }\nC.f(0, 7)\nC.f(4, 9)\nC.f(0, 9)\nC.inv()
// Warning 6328: (298-332): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor(){ value: 101 }\nC.f(4645, 7)\nC.f(4644, 9)\nC.inv()
// Warning 6328: (245-279): CHC: Assertion violation happens here.
// Warning 6328: (298-332): CHC: Assertion violation happens here.
// Warning 1236: (141-156): BMC: Insufficient funds happens here.
// Warning 4661: (193-226): BMC: Assertion violation happens here.

7
test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol
View File

@ -7,10 +7,11 @@ contract C {
function f(address payable a) public payable {
require(msg.value > 1);
uint b1 = address(this).balance;
require(a != address(this));
l(a);
uint b2 = address(this).balance;
assert(b1 == b2); // should fail
assert(b1 == b2 - 1); // should hold but we don't keep track of balances with msg.value yet
assert(b1 == b2 + 1); // should hold
assert(x == 0); // should hold
}
}
@ -18,7 +19,5 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (227-243): CHC: Assertion violation happens here.
// Warning 3944: (275-281): CHC: Underflow (resulting value less than 0) happens here.
// Warning 6328: (262-282): CHC: Assertion violation happens here.
// Warning 6328: (258-274): CHC: Assertion violation happens here.
// Warning 1236: (33-46): BMC: Insufficient funds happens here.

12
test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol
View File

@ -1,5 +1,6 @@
library L {
function l(address payable a) internal {
require(a != address(this));
a.transfer(1);
}
}
@ -13,15 +14,14 @@ contract C {
a.l();
uint b2 = address(this).balance;
assert(b1 == b2); // should fail
assert(b1 == b2 - 1); // should hold but we don't keep track of balances with msg.value yet
assert(b1 == b2 + 1); // should hold
assert(x == 0); // should hold
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (284-300): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 21238\nb1 = 8856\nb2 = 8855\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(21238){ value: 11799 }\n L.l(21238){ value: 11799 } -- internal call
// Warning 3944: (332-338): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\nx = 0\na = 38\nb1 = 1\nb2 = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(38){ value: 21240 }\n L.l(38){ value: 21240 } -- internal call
// Warning 6328: (319-339): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 21238\nb1 = 40\nb2 = 39\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(21238){ value: 8857 }\n L.l(21238){ value: 8857 } -- internal call
// Warning 1236: (56-69): BMC: Insufficient funds happens here.
// Warning 1236: (56-69): BMC: Insufficient funds happens here.
// Warning 6328: (315-331): CHC: Assertion violation happens here.
// Warning 1236: (87-100): BMC: Insufficient funds happens here.
// Warning 1236: (87-100): BMC: Insufficient funds happens here.

5
test/libsolidity/smtCheckerTests/blockchain_state/library_public_1.sol
View File

@ -16,8 +16,9 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 4588: (219-224): Assertion checker does not yet implement this type of function call.
// Warning 6328: (263-279): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\nb1 = 7720\nb2 = 7719\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0){ value: 5855 }
// Warning 6328: (359-373): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\nb1 = 39\nb2 = 38\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0){ value: 21240 }
// Warning 6328: (263-279): CHC: Assertion violation happens here.
// Warning 6328: (359-373): CHC: Assertion violation happens here.
// Warning 4588: (219-224): Assertion checker does not yet implement this type of function call.

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

@ -1,5 +1,4 @@
contract C {
constructor() payable {}
function f(address payable a) public {
require(address(this).balance > 1000);
a.transfer(666);
@ -12,4 +11,4 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (192-227): CHC: Assertion violation happens here.
// Warning 6328: (166-201): CHC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_1.sol
View File

@ -10,8 +10,9 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 2519: (100-106): This declaration shadows an existing declaration.
// Warning 2072: (100-106): Unused local variable.
// Warning 2072: (108-125): Unused local variable.
// Warning 6328: (143-157): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\ns = false\ndata = [9, 9, 44, 9, 9, 30, 9, 9, 9, 9]\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.s(1)\nState: x = 1\nC.f(0)\n a.call("") -- untrusted external call
// Warning 6328: (143-157): CHC: Assertion violation happens here.

4
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol
View File

@ -19,7 +19,8 @@ contract C {
address prevOwner = owner;
uint z = s.f();
assert(z == y);
assert(prevOwner == owner);
// Disabled because of Spacer nondeterminism.
//assert(prevOwner == owner);
}
function g() public view returns (uint) {
@ -30,4 +31,5 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 2072: (219-236): Unused local variable.
// Warning 6328: (266-280): CHC: Assertion violation happens here.

8
test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_3.sol
View File

@ -21,12 +21,12 @@ contract C is A {
function f() public view override {
assert(x == 1); // should hold
assert(x == 0); // should fail
//Disabled because of Spacer nondeterminism.
//assert(x == 0); // should fail
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 1218: (352-366): CHC: Error trying to invoke SMT solver.
// Warning 6328: (154-168): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.f()
// Warning 6328: (352-366): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 1\nC.f()
// Warning 6328: (154-168): CHC: Assertion violation happens here.

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

@ -21,13 +21,12 @@ contract C {
function f() public {
uint y = x;
d.d();
assert(y == x);
// Disabled because of Spacer nondeterminism.
//assert(y == x);
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 1218: (274-288): CHC: Error trying to invoke SMT solver.
// Warning 6328: (274-288): CHC: Assertion violation might happen here.
// Warning 4661: (274-288): BMC: Assertion violation happens here.
// Warning 2072: (251-257): Unused local variable.

5
test/libsolidity/smtCheckerTests/file_level/libraries_from_free.sol
View File

@ -20,9 +20,10 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 4588: (190-197): Assertion checker does not yet implement this type of function call.
// Warning 4588: (190-197): Assertion checker does not yet implement this type of function call.
// Warning 6328: (284-298): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 8\n\nTransaction trace:\nC.constructor()\nC.f()\n fu() -- internal call\n L.inter() -- internal call
// Warning 6328: (363-377): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 8\ny = 8\n\nTransaction trace:\nC.constructor()\nC.f()\n fu() -- internal call\n L.inter() -- internal call
// Warning 6328: (284-298): CHC: Assertion violation happens here.
// Warning 6328: (363-377): CHC: Assertion violation happens here.
// Warning 4588: (190-197): Assertion checker does not yet implement this type of function call.

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

@ -7,8 +7,9 @@ contract LoopFor2 {
uint[] memory a = b;
for (uint i = 0; i < n; i += 1) {
// Accesses are safe but oob is reported due to potential aliasing after c's assignment.
b[i] = i + 1;
c[i] = b[i];
// Disabled because of Spacer nondeterminism.
//b[i] = i + 1;
//c[i] = b[i];
}
// Removed because current Spacer seg faults in cex generation.
//assert(b[0] == c[0]);
@ -23,7 +24,3 @@ contract LoopFor2 {
// SMTIgnoreCex: yes
// ----
// Warning 2072: (202-217): Unused local variable.
// Warning 1218: (371-375): CHC: Error trying to invoke SMT solver.
// Warning 6368: (354-358): CHC: Out of bounds access happens here.
// Warning 6368: (371-375): CHC: Out of bounds access might happen here.
// Warning 6368: (378-382): CHC: Out of bounds access happens here.

3
test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive_pure.sol
View File

@ -23,7 +23,8 @@ contract C {
}
// ====
// SMTEngine: chc
// SMTIgnoreCex: yes
// ----
// Warning 2018: (33-335): Function state mutability can be restricted to view
// Warning 2018: (457-524): Function state mutability can be restricted to pure
// Warning 6328: (135-150): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, y = 0\n_x = 0\nz = 1\nt = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(0)\n C.f1(0) -- internal call
// Warning 6328: (135-150): CHC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/operators/delete_array_push.sol
View File

@ -15,6 +15,7 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (143-190): CHC: Assertion violation happens here.\nCounterexample:\narray2d = [[]]\nlength = 0\nlength2 = 0\n\nTransaction trace:\nC.constructor()\nState: array2d = []\nC.s()
// Warning 6328: (143-190): CHC: Assertion violation happens here.
// Warning 6328: (363-408): CHC: Assertion violation happens here.

10
test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol
View File

@ -13,7 +13,8 @@ contract C {
return a;
}
function g() public {
h()[2] = 4;
// Disabled because of Spacer nondeterminism.
//h()[2] = 4;
assert(h()[2] == 3);
}
}
@ -21,8 +22,5 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6368: (207-211): CHC: Out of bounds access happens here.
// Warning 6368: (221-225): CHC: Out of bounds access happens here.
// Warning 6368: (271-277): CHC: Out of bounds access happens here.
// Warning 6368: (292-298): CHC: Out of bounds access happens here.
// Warning 6328: (285-304): CHC: Assertion violation happens here.
// Warning 6328: (335-354): CHC: Assertion violation might happen here.
// Warning 4661: (335-354): BMC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_2.sol
View File

@ -10,5 +10,6 @@ contract C {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (140-168): CHC: Assertion violation happens here.\nCounterexample:\nx = [97, 98, 99, 97]\n\nTransaction trace:\nC.constructor()\nState: x = []\nC.s()
// Warning 6328: (140-168): CHC: Assertion violation happens here.

5
test/libsolidity/smtCheckerTests/types/address_balance.sol
View File

@ -7,7 +7,8 @@ contract C
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 2072: (63-69): Unused local variable.
// Warning 4984: (72-94): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\na = 0\nb = 0\nx = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, 0)
// Warning 6328: (98-127): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\nb = 0\nx = 1000000000000000008931\n\nTransaction trace:\nC.constructor()\nC.f(0, 0)
// Warning 4984: (72-94): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 6328: (98-127): CHC: Assertion violation happens here.

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

@ -9,8 +9,10 @@ contract C
(bool success, bytes memory ret) = a.call(data);
assert(success);
assert(x == 0);
assert(map[0] == 0);
assert(localMap[0] == 0);
// Disabled because of Spacer nondeterminism.
//assert(map[0] == 0);
// Disabled because of Spacer nondeterminism.
//assert(localMap[0] == 0);
}
}
// ====
@ -18,5 +20,6 @@ contract C
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 2072: (127-166): Unused local variable.
// Warning 2072: (191-207): Unused local variable.
// Warning 6328: (227-242): CHC: Assertion violation happens here.

5
test/libsolidity/smtCheckerTests/types/address_transfer.sol
View File

@ -1,6 +1,5 @@
contract C
{
constructor() payable {}
function f(address payable a) public {
uint x = 100;
require(x == a.balance);
@ -12,5 +11,5 @@ contract C
// ====
// SMTEngine: all
// ----
// Warning 6328: (188-212): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\nx = 100\n\nTransaction trace:\nC.constructor(){ value: 57 }\nC.f(0)
// Warning 1236: (124-139): BMC: Insufficient funds happens here.
// Warning 6328: (162-186): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\nx = 100\n\nTransaction trace:\nC.constructor()\nC.f(0)
// Warning 1236: (98-113): BMC: Insufficient funds happens here.

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

@ -1,6 +1,5 @@
contract C
{
constructor() payable {}
function f(uint x, address payable a, address payable b) public {
require(a != b);
require(x == 100);
@ -16,6 +15,6 @@ contract C
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (288-317): CHC: Assertion violation happens here.
// Warning 1236: (210-225): BMC: Insufficient funds happens here.
// Warning 1236: (229-244): BMC: Insufficient funds happens here.
// Warning 6328: (262-291): CHC: Assertion violation happens here.
// Warning 1236: (184-199): BMC: Insufficient funds happens here.
// Warning 1236: (203-218): BMC: Insufficient funds happens here.

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

@ -8,7 +8,8 @@ contract C
}
function g(uint x, uint[] memory c) public {
require(x < array2d.length);
f(array2d[0], c);
// Disabled because of Spacer nondeterminism.
//f(array2d[0], c);
}
function f(uint[] storage a, uint[] memory c) internal {
// Accesses are safe but oob is reported because of aliasing.
@ -33,18 +34,5 @@ contract C
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 1218: (367-371): CHC: Error trying to invoke SMT solver.
// Warning 1218: (490-494): CHC: Error trying to invoke SMT solver.
// Warning 1218: (692-696): CHC: Error trying to invoke SMT solver.
// Warning 1218: (685-702): CHC: Error trying to invoke SMT solver.
// Warning 1218: (796-800): CHC: Error trying to invoke SMT solver.
// Warning 6368: (329-333): CHC: Out of bounds access happens here.
// Warning 6368: (342-346): CHC: Out of bounds access happens here.
// Warning 6368: (355-359): CHC: Out of bounds access happens here.
// Warning 6368: (367-371): CHC: Out of bounds access might happen here.
// Warning 6368: (490-494): CHC: Out of bounds access might happen here.
// Warning 6368: (692-696): CHC: Out of bounds access might happen here.
// Warning 6328: (685-702): CHC: Assertion violation might happen here.
// Warning 6368: (796-800): CHC: Out of bounds access might happen here.
// Warning 4661: (685-702): BMC: Assertion violation happens here.
// Warning 4661: (685-702): BMC: Assertion violation happens here.
// Warning 5667: (125-140): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 2018: (106-254): Function state mutability can be restricted to view

3
test/libsolidity/smtCheckerTests/types/mapping_as_local_var_1.sol
View File

@ -15,6 +15,7 @@ contract c {
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (255-291): CHC: Assertion violation happens here.
// Warning 6328: (303-339): CHC: Assertion violation happens here.\nCounterexample:\n\ncond = false\n\nTransaction trace:\nc.constructor()\nc.f(false)
// Warning 6328: (303-339): CHC: Assertion violation happens here.