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

Update to the tests to combat nondeterminism

Browse Source
This commit is contained in:
Martin Blicha 2023-08-01 20:25:04 +02:00
parent 342df8a515
commit 83b60754a9
2 changed files with 8 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -7,7 +7,7 @@ contract C {
_a.transfer(_v);
}
function inv() public view {
assert(address(this).balance > 0); // should fail
//assert(address(this).balance > 0); // should fail, but commented out because of Spacer nondeterminism
assert(address(this).balance > 80); // should fail
assert(address(this).balance > 90); // should fail
}
@ -16,7 +16,6 @@ contract C {
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (193-226): CHC: Assertion violation happens here.
// Warning 6328: (245-279): CHC: Assertion violation happens here.
// Warning 6328: (298-332): CHC: Assertion violation happens here.
// Warning 6328: (299-333): CHC: Assertion violation happens here.
// Warning 6328: (352-386): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor(){ msg.value: 101 }\nC.f(0x11, 5)\nC.f(0x11, 9)\nC.inv()
// Warning 1236: (141-156): BMC: Insufficient funds happens here.

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

@ -8,8 +8,8 @@ contract LoopFor2 {
function testUnboundedForLoop(uint n) public {
require(n < b.length);
require(n < c.length);
require(n > 0 && n < 100);
b[0] = 900;
require(n > 0 && n < 10);
//b[0] = 900; // Removed because of Spacer's nondeterminism
uint[] storage a = b;
uint i;
while (i < n) {
@ -25,8 +25,7 @@ contract LoopFor2 {
// ====
// SMTEngine: all
// ----
// Warning 6368: (288-292): CHC: Out of bounds access might happen here.
// Warning 6368: (459-463): CHC: Out of bounds access happens here.
// Warning 6328: (452-471): CHC: Assertion violation happens here.
// Warning 6328: (475-494): CHC: Assertion violation happens here.
// Warning 6368: (506-510): CHC: Out of bounds access happens here.\nCounterexample:\nb = [1, 0], c = [0, 0]\nn = 1\na = []\ni = 1\n\nTransaction trace:\nLoopFor2.constructor()\nState: b = [], c = []\nLoopFor2.p()\nState: b = [0], c = [0]\nLoopFor2.p()\nState: b = [0, 0], c = [0, 0]\nLoopFor2.testUnboundedForLoop(1)
// Warning 6328: (499-518): CHC: Assertion violation happens here.\nCounterexample:\nb = [1, 0], c = [0, 0]\nn = 1\ni = 1\n\nTransaction trace:\nLoopFor2.constructor()\nState: b = [], c = []\nLoopFor2.p()\nState: b = [0], c = [0]\nLoopFor2.p()\nState: b = [0, 0], c = [0, 0]\nLoopFor2.testUnboundedForLoop(1)
// Warning 6328: (522-541): CHC: Assertion violation happens here.\nCounterexample:\nb = [1, 0], c = [0, 0]\nn = 1\ni = 1\n\nTransaction trace:\nLoopFor2.constructor()\nState: b = [], c = []\nLoopFor2.p()\nState: b = [0], c = [0]\nLoopFor2.p()\nState: b = [0, 0], c = [0, 0]\nLoopFor2.testUnboundedForLoop(1)
// Info 1391: CHC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.