Function vstd::raw_ptr::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)