search

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

call to undeclared procedure: address_0x... #130

Open dddejan opened 4 years ago

dddejan commented 4 years ago 
pragma solidity >=0.5.0;

contract A {
  address public constant owner = address(0x0CD95a59fAd089c4EBCCEB54f335eC8f61Caa80e);
}
contract B {
  A a;
  function f() public view returns (address b) {
    b = a.owner();
  }
}

Gives

$ solc-verify.py issue.sol --output .
Error while running verifier, details:
Parsing ./issue.sol.bpl
./issue.sol.bpl(33,1): Error: call to undeclared procedure: address_0x0CD95a59fAd089c4EBCCEB54f335eC8f61Caa80e
1 name resolution errors detected in ./issue.sol.bpl

Surprisingly, if I replace the address with 0x0, then I get 

solc-verify.py issue.sol --output .
A::[implicit_constructor]: OK
B::[implicit_constructor]: OK
B::f: SKIPPED
Use --show-warnings to see 1 warning.
Some functions were skipped. Use --verbose to see details.
No errors found.