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

don't havoc constants #128

Closed dddejan closed 4 years ago

dddejan commented 4 years ago
pragma solidity >=0.5.0;
contract A {
  uint constant C = 1;
  function f(address a) public {
    a.call("");
  }
}

Currently does

$ solc-verify.py issue.sol --output .
Error while running verifier, details:
Parsing ./issue.sol.bpl
./issue.sol.bpl(41,7): Error: undeclared identifier: C#4
1 name resolution errors detected in ./issue.sol.bpl

becuase the call hovocs the state (including constant)

call __call_ret#0, __call_ret#1 := __call(a#6, __this, 0);
if (__call_ret#0) {
  havoc C#4; 
  havoc __balance;
}
hajduakos commented 4 years ago

Fixed in d32cf77