[0.7] Wrong result with repacking

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] Wrong result with repacking #161

Closed hajduakos closed 4 years ago

hajduakos commented 4 years ago

structs/LocalStorageRepack.sol reports an assertion failure which should hold.

test/solc-verify/structs/LocalStorageRepack.sol [ --show-warnings ]
1c1,2
< LocalStorageRepack::[fallback]: OK
---
> LocalStorageRepack::[receive]: ERROR
>  - test/solc-verify/structs/LocalStorageRepack.sol:36:9: Assertion might not hold.
3c4
< No errors found.
---
> Errors were found by the verifier.

hajduakos commented 4 years ago

Was tricky to find, but there was a mismatch between indexes due to replacing a loop. Fixed in 530e16a

dddejan commented 4 years ago

Ah sorry about that. I had a feeling that loop replacement was not a good idea but didn't go back to check.