Add contracts for Layout and Alignment #33
Merged
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
celinval
reviewed
Jul 9, 2024
This comment was marked as duplicate.
This comment was marked as duplicate.
Sorry, something went wrong.
This comment was marked as duplicate.
This comment was marked as duplicate.
Sorry, something went wrong.
These contracts seek to capture what is described in documentation and debug assertions.
tautschnig
force-pushed
the
layout-contracts
branch
from
6c60af7 to
1e5ba53
Compare
celinval
reviewed
Jul 10, 2024
feliperodri
reviewed
Jul 11, 2024
celinval
approved these changes
Jul 11, 2024
tautschnig
added a commit
to tautschnig/verify-rust-std
that referenced
this pull request
Jul 23, 2024
In model-checking#33 a contract was added to `Alignment::new_unchecked`, but its verification was only implicit through `Layout`, and may be affected by future changes to the contract that was added to `Layout`. This commit remedies this by adding a separate harness just for `Alignment`.
szlee118
pushed a commit
to stogaru/verify-rust-std
that referenced
this pull request
Oct 17, 2024
These contracts seek to capture what is described in documentation and debug assertions.
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.
These contracts seek to capture what is described in documentation and debug assertions.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.