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

[0.7] Identifier this not available for contract annotations #158

Closed hajduakos closed 4 years ago

hajduakos commented 4 years ago

For example, examples/SumOverStructMember.sol gives

> Error while running compiler, details:
> Warning: This is a pre-release compiler version, please do not use it in production.
> 
> 
> ======= Converting to Boogie IVL =======
> 
> ======= test/solc-verify/examples/SumOverStructMember.sol =======
> Annotation:1:74: solc-verify error: Undeclared identifier. "this" is not (or not yet) visible at this point.
> __verifier_sum_uint(accounts[__verifier_idx_address].balance) <= address(this).balance
>                                                                          ^--^
> test/solc-verify/examples/SumOverStructMember.sol:8:1: solc-verify error: Error(s) while translating annotation for node
> contract Bank {
> ^ (Relevant source part starts here and spans across multiple lines).
> 
dddejan commented 4 years ago

Fixed in ff4badf5b87490eead5be5ca829533042e13fb0b