[kani] Prove some PtrInner methods #2444
Open
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
joshlf
commented
Mar 18, 2025
Comment on lines
+719
to
+807
| // TODO: Assert that `t` and `rest` are contiguous and | ||
| // non-overlapping. |
| } | ||
| } | ||
| Err(CastError::Alignment(_)) => { | ||
| // TODO: Prove that there would have been an alignment problem. |
| // TODO: Prove that there would have been an alignment problem. | ||
| } | ||
| Err(CastError::Size(_)) => { | ||
| // TODO: Prove that there would have been a size problem. |
|
@jswrenn Not yet ready to merge because of a few TODOs, but mostly ready to review. |
joshlf
force-pushed
the
Ic1e352d3d92a45ff86d8ca85b8221bccfb07033b
branch
from
7a5265e to
a48ef98
Compare
Codecov ReportAll modified and coverable lines are covered by tests ✅
Additional details and impacted files@@ Coverage Diff @@
## main #2444 +/- ##
=======================================
Coverage 90.42% 90.42%
=======================================
Files 18 18
Lines 7319 7319
=======================================
Hits 6618 6618
Misses 701 701 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
joshlf
force-pushed
the
Ic1e352d3d92a45ff86d8ca85b8221bccfb07033b
branch
3 times, most recently
from
76f0bfe to
62b30bf
Compare
jswrenn
requested changes
Mar 18, 2025
There was a problem hiding this comment.
Let's pass -Zmem-predicates in our CI runner; then we can make use of kani::same_allocation and the other memory predicates.
joshlf
force-pushed
the
Ic1e352d3d92a45ff86d8ca85b8221bccfb07033b
branch
2 times, most recently
from
badfc70 to
de9ff27
Compare
joshlf
changed the base branch from
main
to
I681bacc2fbc00531c8493490b9f982fa4aea307a
joshlf
force-pushed
the
Ic1e352d3d92a45ff86d8ca85b8221bccfb07033b
branch
from
de9ff27 to
52b2eea
Compare
joshlf
force-pushed
the
I681bacc2fbc00531c8493490b9f982fa4aea307a
branch
from
2a3b116 to
f375ace
Compare
Base automatically changed from
I681bacc2fbc00531c8493490b9f982fa4aea307a
to
main
March 18, 2025 20:59
joshlf
force-pushed
the
Ic1e352d3d92a45ff86d8ca85b8221bccfb07033b
branch
from
52b2eea to
21799ba
Compare
joshlf
changed the base branch from
main
to
Ide939969b8d0c3bc117aa9f1dba06e6d570f262f
joshlf
force-pushed
the
Ide939969b8d0c3bc117aa9f1dba06e6d570f262f
branch
from
6529681 to
40f3f1e
Compare
joshlf
force-pushed
the
Ic1e352d3d92a45ff86d8ca85b8221bccfb07033b
branch
from
21799ba to
94d93fd
Compare
gherrit-pr-id: Ide939969b8d0c3bc117aa9f1dba06e6d570f262f
Also add Kani `requires` and `ensures` annotations to some methods and to some functions in `util`. While we're here, roll Kani to 0.60.0 and fix the Kani roller. gherrit-pr-id: Ic1e352d3d92a45ff86d8ca85b8221bccfb07033b
joshlf
force-pushed
the
Ic1e352d3d92a45ff86d8ca85b8221bccfb07033b
branch
from
94d93fd to
2640e7a
Compare
joshlf
force-pushed
the
Ide939969b8d0c3bc117aa9f1dba06e6d570f262f
branch
from
40f3f1e to
19ae290
Compare
Base automatically changed from
Ide939969b8d0c3bc117aa9f1dba06e6d570f262f
to
main
March 19, 2025 00:23
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.
Also add Kani
requiresandensuresannotations to some methods andto some functions in
util.While we're here, roll Kani to 0.60.0 and fix the Kani roller.
This PR is on branch ptr-kani.