Function vstd::raw_ptr::ptr_mut_write

source · 
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.