Function vstd::raw_ptr::ptr_ref2

source ·

pub exec fn ptr_ref2<'a, T>(
    ptr: *const T,
    verus_tmp_perm: Tracked<&PointsTo<T>>
) -> v : SharedReference<'a, T>

Expand description

requires

perm.ptr() == ptr,

perm.is_init(),

ensures

v.value() == perm.value(),

v.ptr().addr() == ptr.addr(),

v.ptr()@.metadata == ptr@.metadata,

Like ptr_ref but returns a SharedReference so it keeps track of the relationship between the pointers. Note the resulting reference’s pointers does NOT have the same provenance. This is because in Rust models like Stacked Borrows / Tree Borrows, the pointer gets a new tag.

Function vstd::raw_ptr::ptr_ref2Copy item path

Function vstd::raw_ptr::ptr_ref2