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

Base constant access fail #35

Closed dddejan closed 5 years ago

dddejan commented 5 years ago
contract A {
    uint constant x = 2;
}

contract B is A {
    function f() public pure returns (uint) {
        return A.x;
    }
}

Returns

solc-verify.py test/libsolidity/syntaxTests/viewPureChecker/access_to_base_member_constant.sol --output .
Error while running verifier, details:
[TRACE] Using prover: /usr/local/bin/z3
Parsing ./access_to_base_member_constant.sol.bpl
./access_to_base_member_constant.sol.bpl(26,7): Error: undeclared identifier: x#3
1 name resolution errors detected in ./access_to_base_member_constant.sol.bpl
hajduakos commented 5 years ago

Fixed in 37886f6