vstd::raw_ptr

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