Adding test case that fails if contracts can initiate transactions. #255
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…le code. Also guarding code that only allows non-contracts to initiate transactions with a flag that is on by default
|
|
added 10 commits
April 17, 2020 10:07
…ction. Adding an assumption that msgvalue is 0 for all non-payable functions.
…nctions of contract variables in addition to the contract's public functions
…function. Adding a flag to model non-linear arithmetic as an uninterpreted function. Adding preliminary support for super. Function with super now seem to behave correctly
|
The regressions are failing. |
…n infinite loop where you had run out of gas but it was never checked. We not guard against that. Also adding an explicit revert call for the callback model.
…rting uints right now.
… type if modularArithmetic flag is on. Fixed bug with casting down in Modular arithmetic and found bug in VeriSol where it will translate a += foo(b) incorrectly. Added an assertion that will fill if the translation will be incorrect
…, we should check the type of the contract we are making the call to, otherwise we we have a lot of repetition and can make illegal calls. For multipleCallback I'm changing the while loop from while(*) to while(nondet && gas >= 21000)
…ures on an access. It passes all regressions as long as ERC20 recursionDepth=4. I also think it may need a bit more work on nested structure assignment, but we should be able to cross that bridge later.
… rather than a split map if not aliased. All regressions pass in this mode, but there is still some work that needs to be done for the qantFreeAlloc mode. Right now only zero functions are generated but for statically sized arrays, other length initializers might be necessary. Will add this in later.
…all written variables
…e. (bool success, ) = call()
…ld not be included in vars and vars should be in inheritance order.
…public getters for mappings/arrays as it didn't take arguments into account. Have a workaround but only if generating the getters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Adding regression for case where harness can call otherwise unreachable code. Also guarding code that only allows non-contracts to initiate transactions with a flag that is on by default