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

TCCs for array return values #140

Closed dddejan closed 4 years ago

dddejan commented 4 years ago 
$ ./solc-verify.py --arithmetic mod test/solc-verify/arrays/ArraysMem.sol
Error while running verifier, details:
Parsing /var/folders/1k/jf_jw78957j3q1sw49x8vb940000gn/T/tmpdar3y1_r/ArraysMem.sol.bpl
/var/folders/1k/jf_jw78957j3q1sw49x8vb940000gn/T/tmpdar3y1_r/ArraysMem.sol.bpl(21,282): Error: undeclared identifier: x#5
/var/folders/1k/jf_jw78957j3q1sw49x8vb940000gn/T/tmpdar3y1_r/ArraysMem.sol.bpl(21,327): Error: undeclared identifier: x#5
/var/folders/1k/jf_jw78957j3q1sw49x8vb940000gn/T/tmpdar3y1_r/ArraysMem.sol.bpl(22,212): Error: undeclared identifier: x#5
/var/folders/1k/jf_jw78957j3q1sw49x8vb940000gn/T/tmpdar3y1_r/ArraysMem.sol.bpl(22,257): Error: undeclared identifier: x#5
4 name resolution errors detected in /var/folders/1k/jf_jw78957j3q1sw49x8vb940000gn/T/tmpdar3y1_r/ArraysMem.sol.bpl
hajduakos commented 4 years ago

This seems to be a special case of #117, marked it as duplicate

hajduakos commented 4 years ago

Assuming postcondition TCCs (f8adb1b6e3fc181b155c807f1dc7a6c50d9d0916) should now fix this and also #117. Currently all postcondition TCCs are added as an assume instead of preconditions. This way we might not detect if we mess up something with the translation and variables are out of range when calling a function. We could improve this by detecting if a TCC has return value in it and if yes add as assume, otherwise add as precondition.