Function vstd::raw_ptr::ptr_mut_write

pub exec fn ptr_mut_write<T>(
    ptr: *mut T,
    verus_tmp_perm: Tracked<&mut PointsTo<T>>,
    v: T
)

Expand description

requires

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

old(perm).is_uninit(),

ensures

perm.ptr() == ptr,

perm.opt_value() == MemContents::Init(v),

Calls core::ptr::write

This does not drop the contents. If the memory is already initialized and you want to write without dropping, call PointsTo::leak_contents first.

Function vstd::raw_ptr::ptr_mut_writeCopy item path