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

Side effects for default values #114

Open hajduakos opened 4 years ago

hajduakos commented 4 years ago

Currently the helper function for default values returns simply an expression. However, in many cases default values have side effects: e.g., allocation, element/member initialization, which is currently done "manually" all around the code. Instead, the default value helpershould be able to return statements (and maybe declarations) as side effect. This would make it easier to implement default values for reference types in memory, especially nested structs/arrays. See e.g., #102