Closed
Description
Requested feature: Create a method to ensure a pointer is valid.
Use case: Verifying unsafe operations
Link to relevant documentation (Rust reference, Nomicon, RFC):
The method I was thinking would be something like:
pub fn is_ptr_valid<T: ?Sized>(ptr: *const T) -> bool {
let sz = intrinsics::size_of_val(ptr);
// Kani intrinsic that translates to __CPROVER_r_ok
is_read_ok(ptr, sz)
}