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

Make counterexample deterministic

Browse Source
This commit is contained in:
Martin Blicha 2023-07-27 16:22:55 +02:00
parent 4ecaa476fd
commit 799f418bef
1 changed files with 3 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol
View File

@ -14,6 +14,7 @@ contract C {
} }
function f(address _a) public { function f(address _a) public {
require(x == 0);
uint y = x; uint y = x;
_a.call("aaaaa"); _a.call("aaaaa");
assert(y == x); // should fail assert(y == x); // should fail
@ -23,5 +24,5 @@ contract C {
// SMTEngine: all // SMTEngine: all
// SMTIgnoreCex: no // SMTIgnoreCex: no
// ---- // ----
// Warning 9302: (212-228): Return value of low-level calls not used. // Warning 9302: (231-247): Return value of low-level calls not used.
// Warning 6328: (232-246): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, lock = false\n_a = 0x0\ny = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0, lock = false\nC.set(1)\nState: x = 1, lock = false\nC.f(0x0)\n _a.call("aaaaa") -- untrusted external call, synthesized as:\n C.set(0) -- reentrant call // Warning 6328: (251-265): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, lock = false\n_a = 0x0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, lock = false\nC.f(0x0)\n _a.call("aaaaa") -- untrusted external call, synthesized as:\n C.set(1) -- reentrant call