Function vstd::raw_ptr::ptr_ref

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

equivalent to &*X