Create an API to check valid raw pointer

[celinval]

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)
}

[adpaco-aws]

#1496 is less detailed but looks similar

[celinval]

I'll update #1496 and close this one since there's some interesting discussions there. Thanks @adpaco-aws!

[celinval]

Reopening this one, since __CPROVER_r_ok does not match the behavior requested in this issue.

[celinval]

Note that this is blocked since there is no way to encode this in CBMC today. I've created a request here: https://github.com/diffblue/cbmc/issues/8217

[feliperodri]

https://github.com/model-checking/kani/pull/3107 solves this issue.