search

ethereum / solidity

Solidity, the Smart Contract Programming Language
https://soliditylang.org
GNU General Public License v3.0
23.3k stars 5.77k forks source link

Fail to generate why3 source with --formal #943

Closed chatch closed 8 years ago

chatch commented 8 years ago

Running "solc --formal" against Fund.sol from this gist results in an error "Compound assignment not supported".

formal> solc --version solc, the solidity compiler commandline interface Version: 0.3.6-0/None-Linux/g++

formal> solc --formal Fund.sol Fund.sol:6:13: Error: Compound assignment not supported. shares -= amount; // subtract the amount from the shares ^--------------^

My version of solc is the latest in the ethereum ppa.

chatch commented 8 years ago

I can workaround this by expanding the assignment to "shares = shares - amount;"

chriseth commented 8 years ago

Yes, the gist is an old example, the syntax changed in the meantime. Please use this example: https://chriseth.github.io/notes/talks/formal_ic3_bootcamp/#/7