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

complex modifiers and variable redeclarations #131

Closed dddejan closed 4 years ago

dddejan commented 4 years ago
pragma solidity >=0.5.0;

contract A {

  mapping(address=>uint) b1;
  mapping(address=>uint) b2;
  mapping(address=>uint) b3;

  modifier min(uint m) {
    address _sender = msg.sender;
    if (b1[_sender] >= m) {
      _;
    } else if (b2[_sender] >= m) {
      _;
    }
  }

  function f() min(100) public {
    address _sender = msg.sender;
    b3[_sender] += 1;
  }
}

Gives

$ solc-verify.py issue.sol --output .
Error while running verifier, details:
Parsing ./issue.sol.bpl
./issue.sol.bpl(28,58): Error: more than one declaration of variable name: _sender#46
1 name resolution errors detected in ./issue.sol.bpl
hajduakos commented 4 years ago

We had extra scoping for inlined modifiers, but not for the inlined function body. Fixed in 71f70b9.