mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
b0419da654
Previously, we did not remember trusted external calls for later phase when we compute possible verification targets for each function. This led to false negative in cases where verification target can be violated, but not by calling a public function directly, but only when it is called as an external function from other function. The added test cases witnesses this behaviour. The underflow in `dec` cannot happen in any other way except what the `dec` is called from `f`. The same problem did not occur when the functions are called internally, because for such cases, we have already been remembering these calls in the callgraph in the CHC engine.
29 lines
956 B
Solidity
29 lines
956 B
Solidity
contract D {
|
|
uint x;
|
|
function inc() public { ++x; }
|
|
function f() public view returns (uint) { return x; }
|
|
}
|
|
|
|
contract C {
|
|
function f() public {
|
|
D d = new D();
|
|
assert(d.f() == 0); // should hold
|
|
d.inc();
|
|
assert(d.f() == 1); // should hold
|
|
d = new D();
|
|
assert(d.f() == 0); // should hold
|
|
assert(d.f() == 1); // should fail
|
|
}
|
|
}
|
|
// ====
|
|
// SMTEngine: all
|
|
// SMTExtCalls: trusted
|
|
// SMTIgnoreOS: macos
|
|
// ----
|
|
// Warning 4984: (47-50): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
|
|
// Warning 6328: (215-233): CHC: Assertion violation might happen here.
|
|
// Warning 6328: (304-322): CHC: Assertion violation happens here.
|
|
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
|
|
// Warning 2661: (47-50): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
|
|
// Warning 4661: (215-233): BMC: Assertion violation happens here.
|