cerc-io/solidity
11
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

Fix false positive on external calls from constructors

Browse Source
This commit is contained in:
Leo Alt
2021-08-12 18:51:55 +02:00
parent 23b16a1e20
commit 6ee60aa628
5 changed files with 22 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files
test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1.sol
+1 -1
View File
@@ -16,4 +16,4 @@ contract C {
// SMTEngine: all
// ----
// Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100)
// Warning 6328: (177-191): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 3\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 3\nC.f()
// Warning 6328: (177-191): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 0\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 0\nC.f()
test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol
+1 -1
View File
@@ -20,4 +20,4 @@ contract C {
// SMTEngine: all
// ----
// Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100)
// Warning 6328: (203-217): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 0\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 0\nC.f()
// Warning 6328: (203-217): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 3\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 3\nC.f()
test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_reentrancy_1.sol
+15
View File
@@ -0,0 +1,15 @@
interface D {
function ext(C c) external returns (uint);
}
contract C {
uint x;
function s(uint _x) public { x = _x; }
constructor(D d) {
uint a = d.ext(this);
assert(x == 0); // should hold because there's no reentrancy from the constructor
assert(a == 2); // should fail
}
}
// ----
// Warning 6328: (253-267): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\nd = 0\na = 3\n\nTransaction trace:\nC.constructor(0)