Function ptr_mut_read_at

Source

pub exec fn ptr_mut_read_at<V, const N: usize>(
    ptr: *mut [V; N],
    verus_tmp_perm: Tracked<&mut PointsToArray<V, N>>,
    index: usize,
) -> res : Vwhere
    V: Copy,

Expand description

requires

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

old(perm).is_init(index as int),

index < N,

ensures

perm.ptr() == ptr,

perm.is_uninit(index as int),

forall |i: int| {
    0 <= i < N && i != index ==> perm.opt_value()[i] == old(perm).opt_value()[i]
},

res == old(perm).opt_value()[index as int].value(),

Read only once and the value will be moved out side of the array

ptr_mut_read_at

Function ptr_mut_read_at Copy item path

Function ptr_mut_read_at