Function ptr_mut_fill

Source

pub exec fn ptr_mut_fill<V, const N: usize>(
    ptr: *mut [V; N],
    verus_tmp_perm: Tracked<&mut PointsToArray<V, N>>,
    value: V,
)where
    V: Copy,

Expand description

requires

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

old(perm).is_uninit_all(),

ensures

perm.ptr() == ptr,

perm.is_init_all(),

forall |i: int| 0 <= i < N ==> perm.opt_value()[i] == raw_ptr::MemContents::Init(value),

Reading and writing to an array of values

ptr_mut_fill

Function ptr_mut_fill Copy item path

Function ptr_mut_fill