Constant propagation for negative numbers

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

Constant propagation for negative numbers #36

Closed hajduakos closed 5 years ago

hajduakos commented 5 years ago

RationalNumberType always returns an unsigned result. If the number is negative, we have to convert it. For example, the result of 2-3 on 8 bits is 255.

hajduakos commented 5 years ago

Fixed in 265665b