vstd::raw_ptr

Function ptr_mut_read

Source 
pub exec fn ptr_mut_read<T>(
    ptr: *const T,
    verus_tmp_perm: Tracked<&mut PointsTo<T>>,
) -> v : T
Expand description
requires
old(perm).ptr() == ptr,
old(perm).is_init(),
ensures
perm.ptr() == ptr,
perm.is_uninit(),
v == old(perm).value(),

core::ptr::read

This leaves the data as “unitialized”, i.e., performs a move.

TODO This needs to be made more general (i.e., should be able to read a Copy type without destroying it; should be able to leave the bytes intact without uninitializing them)