SRI-CSL / solidity

This is solc-verify, a modular verifier for Solidity.
https://github.com/SRI-CSL/solidity/blob/boogie/SOLC-VERIFY-README.md
GNU General Public License v3.0
50 stars 14 forks source link

Havoc contract balance for external calls #115

Closed hajduakos closed 4 years ago

hajduakos commented 4 years ago

When an external call is made, we havoc state variables, but not the balance:

contract ExtCallBalance {
    function g() public payable {
    }

    function f() public {
        uint oldBal = address(this).balance; // Old balance
        msg.sender.call(""); // We make an external call with no value

        // But this should fail because callbacks can modify balance
        assert(oldBal == address(this).balance);
    }
}
hajduakos commented 4 years ago

And since we are havocing state vars, the sum shadow variables should also be havoced

hajduakos commented 4 years ago

Fixed in 7ea853b