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

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

final(perm).is_init_all(),

forall |i: int| {
    0 <= i < N ==> final(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