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(),
ensuresv == perm.value(),
Equivalent to &*ptr
, passing in a permission perm
to ensure safety.
The memory pointed to by ptr
must be initialized.