-
Notifications
You must be signed in to change notification settings - Fork 39
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
CERT-7022 Add Reset Storage + Hook Example #132
CERT-7022 Add Reset Storage + Hook Example #132
Conversation
certoraRun BankReset.conf | ||
``` | ||
|
||
3. **Check the Output**: The execution show that the rule `resetZeroesAllFunds` passes, and the hook `Sstore` for `dontUseMe` is never triggered as expected. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The execution shows
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done
|
||
### Execution Link | ||
|
||
For an example of the output, you can check the execution link: [Certora Run Output](https://prover.certora.com/output/1512/985319a08a424a6e81b8e1dcd9836848?anonymousKey=0ee6ab56949403b32b14f84c4d76ac08eb9acede) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Example of the output attached below:
Example of the output can be seen in the execution link:
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done
|
||
## Overview | ||
|
||
This repository contains an example that demonstrates how hooks behave in CVL when the `reset_storage` command is used. The example uses a simple Solidity contract named `BankReset` and a CVL specification to show that hooks do not get triggered when storage is reset. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
need to give a small explanation of rest_storage as this is not even in the dcouemntation.
reset_storage restore to after constructor or just all zero? are ghost also restored? can we add more to this example? it can be a later task. will this pass if in the constructor the msg.sender is allocated funds?
make sure to update the index page as well
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'll add tickets for both Documentation and Example.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
https://certora.atlassian.net/browse/CERT-7022