pub fn can_dereference<T: ?Sized>(ptr: *const T) -> bool
Expand description
Checks that pointer ptr
point to a valid value of type T
.
For that, the pointer has to be a valid pointer according to crate::mem conditions 1, 2
and 3,
and the value stored must respect the validity invariants for type T
.
TODO: Kani should automatically add those checks when a de-reference happens. https://github.com/model-checking/kani/issues/2975
This function will panic today if the pointer is not null, and it points to an unallocated or deallocated memory location. This is an existing Kani limitation. See https://github.com/model-checking/kani/issues/2690 for more details.