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

Struct and constructors from other contracts #129

Closed dddejan closed 4 years ago

dddejan commented 4 years ago
pragma solidity >=0.5.0;
contract A {
  struct S {
    int x;
  }
}
contract B {
  function f() public pure returns (int) {
    A.S memory s = A.S(0);
    return s.x;
  }
}

Gives

$ solc-verify.py issue.sol --output .
Error while running verifier, details:
Parsing ./issue.sol.bpl
./issue.sol.bpl(43,1): Error: call to undeclared procedure: S#4
./issue.sol.bpl(43,23): Error: undeclared identifier: A#5
2 name resolution errors detected in ./issue.sol.bpl
hajduakos commented 4 years ago

Fixed in edf21dc