Add constructor preserved block documentation#445
Add constructor preserved block documentation#445srunquist-certora merged 2 commits intorelease/version_8.5.1from
Conversation
docs/cvl/invariants.md
Outdated
| If there is no method signature, the preserved block is a default block that is | ||
| used for all methods that don't have a specific preserved block, including the | ||
| `fallback()` method. If an invariant has both a default preserved block and a | ||
| `fallback()` method, but not the constructor. | ||
| If an invariant has both a default preserved block and a |
There was a problem hiding this comment.
I think we can write this more explicit. Wdyt?
A method block with no method signature is called the generic preserved block. The generic preserved block is used for all methods that don't have a specific preserved block, including the
fallback()method. Note, the generic preserved block is not applied for the induction base step, for the induction base step usepreserved constructorinstead.
There was a problem hiding this comment.
Very nice. I also updated the whole section to call it "generic" and not sometimes "default", since that just seemed inconsistent and confusing.
|
@johspaeth - could you take another look and approve? We are working on getting the linkage fixed with ReadTheDocs, but the build did work ok. You can see the content here. If we don't get the docs integration fixed today, I can force merge this PR (once approved). |
srunquist-certora
changed the base branch from
master
to
release/version_8.5.1
* Add constructor preserved block documentation (#445) Adds documentation for document Certora/EVMVerifier#8117 * Update changelog for version 8.5.1 (#449) --------- Co-authored-by: christiane-certora <christiane@certora.com>
3 participants
to document https://github.com/Certora/EVMVerifier/pull/8117
Naming convention:
Before requesting review:
spelling_wordlist.txtREADME.mdfor information about style and markdown syntaxJira ticket: TODO
Link to generated documentation: TODO