search

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

Quantifiers and TCCs #143

Closed dddejan closed 4 years ago

dddejan commented 4 years ago 
$ solc-verify.py test/solc-verify/specs/Quantifiers.sol --arithmetic mod
Error while running verifier, details:
Parsing /var/folders/3h/8n83hkk15kn72vl2_8bsw18c0000gp/T/tmpqvr4vl6n/Quantifiers.sol.bpl
/var/folders/3h/8n83hkk15kn72vl2_8bsw18c0000gp/T/tmpqvr4vl6n/Quantifiers.sol.bpl(21,217): Error: undeclared identifier: i#186
/var/folders/3h/8n83hkk15kn72vl2_8bsw18c0000gp/T/tmpqvr4vl6n/Quantifiers.sol.bpl(21,228): Error: undeclared identifier: i#186
/var/folders/3h/8n83hkk15kn72vl2_8bsw18c0000gp/T/tmpqvr4vl6n/Quantifiers.sol.bpl(22,326): Error: undeclared identifier: i#186

The quantified variables should include TCCs by default, regardless of any options.

dddejan commented 4 years ago

This is much more complicated then I first though. @hajduakos let's discuss.

hajduakos commented 4 years ago

This seems to be working on the merge branch. At least there are no syntax errors related to missing identifiers. Verification succeeds: there are some specs that do not hold, but those seem acceptable. @dddejan could you check and close the issue?