ptr_mut_write_at

vstd_extra::array_ptr

Function ptr_mut_write_at 

Source 
pub exec fn ptr_mut_write_at<V, const N: usize>(
    ptr: *mut [V; N],
    verus_tmp_perm: Tracked<&mut PointsToArray<V, N>>,
    index: usize,
    value: V,
)
Expand description
requires
old(perm).ptr() == ptr,
old(perm).is_uninit(index as int),
index < N,
ensures
perm.ptr() == ptr,
perm.is_init(index as int),
forall |i: int| {
    0 <= i < N && i != index ==> perm.opt_value()[i] == old(perm).opt_value()[i]
},
perm.opt_value()[index as int] == raw_ptr::MemContents::Init(value),