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 visible for function annotations #154

Closed hajduakos closed 4 years ago

hajduakos commented 4 years ago

Seems like this is not available for function annotations.

For example arrays/ArraysPushPop.sol gives

> ======= Converting to Boogie IVL =======
> 
> ======= test/solc-verify/arrays/ArraysPushPop.sol =======
> Annotation:1:9: solc-verify error: Undeclared identifier. "this" is not (or not yet) visible at this point.
> address(this).balance
>         ^--^