Function can_dereference

Source
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.