Skip to main content

ptr_mut_ref

vstd::raw_ptr

Function ptr_mut_ref 

Source 
pub exec fn ptr_mut_ref<T>(
    ptr: *mut T,
    verus_tmp_perm: Tracked<&mut PointsTo<T>>,
) -> v : &mut T
Expand description
requires
old(perm).ptr() == ptr,
old(perm).is_init(),
ensures
final(perm).ptr() == ptr,
final(perm).is_init(),
old(perm).value() == *v,
final(perm).value() == *final(v),

Equivalent to &mut *X, passing in a permission perm to ensure safety. The memory pointed to by ptr must be initialized.