vstd::raw_ptr

Function 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,
ensures
perm.ptr() == ptr,
perm.opt_value() == MemContents::Init(v),

Calls core::ptr::write to write the value v to the memory location pointed to by ptr, using the permission perm.

This does not drop the contents. If the memory is already initialized, this could leak allocations or resources, so care should be taken to not overwrite an object that should be dropped. This is appropriate for initializing uninitialized memory, or overwriting memory that has previously been read from.