-
Notifications
You must be signed in to change notification settings - Fork 25
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
Assignable free #3188
Merged
Merged
Assignable free #3188
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
Codecov Report
@@ Coverage Diff @@
## main #3188 +/- ##
============================================
+ Coverage 37.59% 37.61% +0.01%
- Complexity 16684 16709 +25
============================================
Files 2043 2043
Lines 125713 125902 +189
Branches 21106 21138 +32
============================================
+ Hits 47257 47353 +96
- Misses 72693 72770 +77
- Partials 5763 5779 +16
... and 1 file with indirect coverage changes 📣 We’re building smart automated test selection to slash your CI/CD build times. Learn more |
mattulbrich
approved these changes
Jul 15, 2023
Rather a large addition to the code. Thanks for your efforts. |
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.
This branch implements
assignable_free
clauses, which akin toensures_free
allow you to specify frame conditions that the caller can assume but the callee does not have to prove. See #3185.assignable_free
clauses are implemented for functional method contracts, functional block/loop contracts, and loop invariants.Semantics
Consider the following example.
Both contracts are provable: The proof obligation for
bar()
must show that onlyfield
is modified, but then whenbar()
is called fromfoo()
,foo()
assumes thatbar()
modifies\nothing
.In general, the caller assumes that the callee only modifies the locations mentioned in its
assignable
clause(s), while the callee must prove that it only modifies the locations in the union of itsassignable
andassignable_free
clauses.