evmverif does not capture the fund moves with selfdestruct

pirapira / evmverif

An EVM code verification framework in Coq

Apache License 2.0

44 stars 8 forks source link

evmverif does not capture the fund moves with selfdestruct #4

Open pirapira opened 7 years ago

pirapira commented 7 years ago

Currently the build_venv_ functions assume that the balance does not change while the contract is not executing. However, there are cases where the account's balance increase while the contract is not executing.