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

constructor calls with additional msg parameters #132

Open dddejan opened 4 years ago

dddejan commented 4 years ago
pragma solidity >=0.5.0;

contract A {
  constructor() public payable {}
}

contract B {
  A a;
  constructor() public payable {
    a = (new A).value(msg.value)();
  }
}

Gives

$ solc-verify.py issue.sol --output .
Error while running verifier, details:
Parsing ./issue.sol.bpl
./issue.sol.bpl(44,1): Error: wrong number of result variables in call to __constructor#6: 1
1 name resolution errors detected in ./issue.sol.bpl