Function vstd::raw_ptr::ptr_ref

source · 
pub exec fn ptr_ref<T>(ptr: *const T, Tracked(perm): Tracked<&PointsTo<T>>) -> v : &T
Expand description
requires
perm.ptr() == ptr,
perm.is_init(),
ensures
v == perm.value(),

equivalent to &*X