Function ptr_mut_read_all

pub exec fn ptr_mut_read_all<V, const N: usize>(
    ptr: *mut [V; N],
    Tracked(perm): Tracked<&mut PointsToArray<V, N>>,
) -> res : [V; N]

Expand description

requires

old(perm).ptr() == ptr,

old(perm).is_init_all(),

ensures

final(perm).ptr() == ptr,

final(perm).is_uninit_all(),

res@ == old(perm).value(),

ptr_mut_read_all