ptr_mut_read_all

vstd_extra::array_ptr

Function ptr_mut_read_all 

Source 
pub exec fn ptr_mut_read_all<V, const N: usize>(
    ptr: *mut [V; N],
    verus_tmp_perm: Tracked<&mut PointsToArray<V, N>>,
) -> res : [V; N]
Expand description
requires
old(perm).ptr() == ptr,
old(perm).is_init_all(),
ensures
perm.ptr() == ptr,
perm.is_uninit_all(),
res@ == old(perm).value(),