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(),
ensuresperm.ptr() == ptr,
perm.is_uninit(),
v == old(perm).value(),
Calls core::ptr::read
to read from the memory pointed to by ptr
,
using the permission perm
.
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).