mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Update test nondet
This commit is contained in:
parent
5c3b5f86f3
commit
d828aeee23
@ -14,7 +14,7 @@ contract LoopFor2 {
|
||||
uint i;
|
||||
while (i < n) {
|
||||
b[i] = i + 1;
|
||||
c[i] = b[i];
|
||||
//c[i] = b[i]; // Removed because of Spacer's nondeterminism
|
||||
++i;
|
||||
}
|
||||
//assert(b[0] == c[0]); // Removed because of Spacer's nondeterminism
|
||||
@ -26,8 +26,6 @@ contract LoopFor2 {
|
||||
// SMTEngine: all
|
||||
// ----
|
||||
// Warning 6368: (288-292): CHC: Out of bounds access might happen here.
|
||||
// Warning 6368: (312-316): CHC: Out of bounds access might happen here.
|
||||
// Warning 6368: (305-309): CHC: Out of bounds access might happen here.
|
||||
// Warning 6368: (411-415): CHC: Out of bounds access happens here.\nCounterexample:\nb = [1, 0], c = [1, 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: (404-423): CHC: Assertion violation happens here.\nCounterexample:\nb = [1, 0], c = [1, 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: (427-446): CHC: Assertion violation happens here.\nCounterexample:\nb = [1, 0], c = [1, 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 6368: (459-463): 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: (452-471): 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: (475-494): 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)
|
||||
|
Loading…
Reference in New Issue
Block a user