Add an example for internal function calls #191
Merged
Conversation
This file contains hidden or 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
Contributor
|
Fyi - the process here is to merge to |
johspaeth
approved these changes
Aug 4, 2025
Contributor
johspaeth
left a comment
johspaeth
left a comment
There was a problem hiding this comment.
LGTM, tiny nit that you can just apply.
@yoav-el-certora for now, this is an internal announcement only. Should we proceed in merging or rather merge when we announce it publicly as well? Please let Naftali know.
Co-authored-by: Johannes Späth <johspaeth@users.noreply.github.com>
yoav-el-certora
added a commit
that referenced
this pull request
Aug 11, 2025
* Add an example on how to reason about events in CVL (#174) * 7.26.0 Release (#163) * Niv/cert 8248 revert example (#155) * CERT 8248 Add Revert Example * Update README * Address Christiane review * Update example based on Nurit Review * Clean * Update config.yml (#160) Co-authored-by: yoav-el-certora <122207807+yoav-el-certora@users.noreply.github.com> * Example ready * christiane cr * Code reviews --------- Co-authored-by: Niv vaknin <122722245+nivcertora@users.noreply.github.com> Co-authored-by: liav-certora <114004726+liav-certora@users.noreply.github.com> Co-authored-by: liav-certora <liav@certora.com> * Bug fixed * Add an example on how to reason about events in CVL * Addressing code reviews * Addressing Christiane's CR * Issue with merge resolution * Revert "Bug fixed" This reverts commit 33b87b9. * Reverse incorrect change after merge --------- Co-authored-by: yoav-el-certora <122207807+yoav-el-certora@users.noreply.github.com> Co-authored-by: Niv vaknin <122722245+nivcertora@users.noreply.github.com> Co-authored-by: liav-certora <114004726+liav-certora@users.noreply.github.com> Co-authored-by: liav-certora <liav@certora.com> Co-authored-by: Otakar <Otakar@certora.com> * Removed Process from conf file * Removed send_only from conf file * add a simple example with a transient field and hooks and direct storage accesses on it * remove rule sanity Co-authored-by: Johannes Späth <johspaeth@users.noreply.github.com> * remove ambiguity * CERT 8687 Realistic example (#167) * CERT 8687 Realistic example * fix spec, sanity issue * fix * require invariant example * Update README * Update CVLByExample/Invariant/RequireInvariantArray/README.md * Addressing Nurit's CR --------- Co-authored-by: Nurit Dor <57101353+nd-certora@users.noreply.github.com> Co-authored-by: Johannes Späth <johspaeth@users.noreply.github.com> Co-authored-by: Johannes Spaeth <johannes@certora.com> * Re routing example (#180) * Re routing example * Updating example --------- Co-authored-by: Johannes Spaeth <johannes@certora.com> * Niv/fix sanity failure (#183) * Fix some of the sanity failure * Fixing specification to not have sanity failures runFullPool.conf -> https://vaas-stg.certora.com/output/53900/a7ab7f221da84eb4accea1c95e936803?anonymousKey=e063b8e60bae944b4a9d0d0431999b5bd4b578ea runBroken.con -> https://vaas-stg.certora.com/output/53900/c85b8c49fec24d32ac0de00043d7ddd6?anonymousKey=a6c585f91d010a7c13f1c6d8935143b894a0c05d * Updates to spec * Self-Review --------- Co-authored-by: Johannes Spaeth <johannes@certora.com> Co-authored-by: yoav-el-certora <122207807+yoav-el-certora@users.noreply.github.com> * Added fixes to breaking changes (#190) * foundry toml * comment * branch * branch * branch * Add an example for internal function calls (#191) * add an example for internal function calls * Update CVLByExample/InternalFunctionsFromCVL/README.md Co-authored-by: Johannes Späth <johspaeth@users.noreply.github.com> --------- Co-authored-by: Johannes Späth <johspaeth@users.noreply.github.com> * Added foundry installation to CI (#194) --------- Co-authored-by: Johannes Späth <johspaeth@users.noreply.github.com> Co-authored-by: Niv vaknin <122722245+nivcertora@users.noreply.github.com> Co-authored-by: liav-certora <114004726+liav-certora@users.noreply.github.com> Co-authored-by: liav-certora <liav@certora.com> Co-authored-by: Otakar <Otakar@certora.com> Co-authored-by: Christiane Goltz <christiane@certora.com> Co-authored-by: Nurit Dor <57101353+nd-certora@users.noreply.github.com> Co-authored-by: Johannes Spaeth <johannes@certora.com> Co-authored-by: rahav <rahav@certora.com> Co-authored-by: Rahav <103361134+rahav-certora@users.noreply.github.com> Co-authored-by: Naftali Goldstein <44599898+naftali-g@users.noreply.github.com>
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.
No description provided.