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

Undeclared constants in generated Boogie code. #49

Closed michael-emmi closed 5 years ago

michael-emmi commented 5 years ago
$ cat Test.sol && solc-verify.py Test.sol --output .
pragma solidity ^0.5.0;

contract Test {
    uint constant C = 42;
    mapping(uint => bool) M;
}
Error while running verifier, details:
[TRACE] Using prover: /usr/local/bin/z3
Parsing ./Test.sol.bpl
./Test.sol.bpl(20,34): Error: undeclared identifier: C#4
1 name resolution errors detected in ./Test.sol.bpl
hajduakos commented 5 years ago

Constants were not inlined when collecting variables of a given type (to initialize arrays/mappings), fixed in 2a85e3a