Add safety preconditions to alloc/src/collections/binary_heap/mod.rs#120
Conversation
This diff adds `#[requires(...)]` attributes to the unsafe functions, translating the "SAFETY:" comments into code contracts. These contracts specify the preconditions that must be met for the function to be safely called.
tautschnig
force-pushed
the
bedrock-library/alloc/src/collections/binary_heap/mod.rs
branch
from
29b2c87 to
8e6b212
Compare
Just as previously done for core: this will enable future use of
`safety::{ensures,requires}` in those crates.
There was a problem hiding this comment.
Do these function require self to be safe?
There was a problem hiding this comment.
Are you asking whether there are requirements that the object is in some sort of sane state? I would believe so, but why would we ever permit for that not to be the case?
There was a problem hiding this comment.
I agree that we shouldn't, but we do.
Conceptually, internal functions can temporary break the safety invariants of the types.
| mod verify { | ||
| use super::*; | ||
|
|
||
| // TODO: Kani reports as failing property "Only a single top-level call", which does not |
There was a problem hiding this comment.
Following up on this: can you extend the TODO to say what function it's complaining about for the single top-level call?
There was a problem hiding this comment.
Otherwise, this PR LGTM, but I am curious if we can do a bit of debugging on this harness before merging it as a TODO. If we really get stuck, I'll approve.
…/src/collections/binary_heap/mod.rs
3 participants
This diff adds
#[requires(...)]attributes to the unsafe functions, translating the "SAFETY:" comments into code contracts. These contracts specify the preconditions that must be met for the function to be safely called.