Contracts & Harnesses for non_null::new and non_null::new_unchecked
#88
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
QinyuanWu
changed the title
non_null::new and non_null::new_uncheckednon_null::new and non_null::new_unchecked
QinyuanWu
changed the title
non_null::new and non_null::new_uncheckednon_null::new and non_null::new_unchecked
zhassan-aws
reviewed
Sep 20, 2024
|
@zhassan-aws if everything else looks good I will squash the commits. |
No need to. We squash on merge. |
|
@zhassan-aws Thank you! Do we need another reviewer for approval to merge? |
|
Yes. |
celinval
requested changes
Sep 24, 2024
There was a problem hiding this comment.
I think it would be great to have harnesses that covers all possible values of the raw pointer. Something like:
let ptr = kani::any::<usize>() as *mut i32;
let _ = NonNull::new_unchecked(ptr);Note that we cannot use the same strategy for functions where we need to ensure pointer validity.
celinval
reviewed
Sep 27, 2024
feliperodri
changed the title
non_null::new and non_null::new_uncheckednon_null::new and non_null::new_unchecked
szlee118
pushed a commit
to stogaru/verify-rust-std
that referenced
this pull request
Oct 17, 2024
…d` (model-checking#88) Towards model-checking#53 ### Changes - added contract and harness for `non_null::new` - added contract and harness for `non_null::new_unchecked` The difference between the two APIs is that `non_null::new` can handle null pointers while `non_null::new_unchecked` does not. Therefore the contract for `non_null::new` does not require a `nonnull` pointer. ### Re-validation To re-validate the verification results, run `kani verify-std -Z unstable-options "path/to/library" -Z function-contracts -Z mem-predicates --harness ptr::non_null::verify::non_null_check_new`. This will run both harnesses. All default checks should pass. --------- Co-authored-by: OwO <owo@OwOs-MacBook-Pro.local> Co-authored-by: Zyad Hassan <88045115+zhassan-aws@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.
Towards #53
Changes
non_null::newnon_null::new_uncheckedThe difference between the two APIs is that
non_null::newcan handle null pointers whilenon_null::new_uncheckeddoes not. Therefore the contract fornon_null::newdoes not require a nonnull pointer.Revalidation
To revalidate the verification results, run
kani verify-std -Z unstable-options "path/to/library" -Z function-contracts -Z mem-predicates --harness ptr::non_null::verify::non_null_check_new. This will run both harnesses. All default checks should pass: