You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
**Do not merge this PR** -- it is just meant for reviews and a CI check,
and then we'll push to main directly instead.
Some callouts:
- The changes to `const_ptr`, `mut_ptr`, and `nonnull` are necessary
because model-checking/kani#3755 introduced a
Kani model for `offset`, which expanded the range of UB that Kani can
catch. It also introduced these failures under the "safety check" label,
which is not affected by `#{should_panic]`. These updates exposed issues
with the existing contracts and proofs (most notably for ZSTs) which are
fixed here.
- A few of the proofs are still failing because of bug(s) in Kani's
function contracts. See
model-checking/kani#3905 for a tracking issue.
For now, they're commented out with a FIXME tag.
Note that the VeriFast failures are expected, since part of its CI job
checks if its proofs are up-to-date with the most recent version of the
library, and the subtree update makes it so that's not the case.
By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---------
Co-authored-by: gitbot <git@bot>
0 commit comments