Skip to main content

pcell_borrow_mut

vstd_extra::auxiliary

Function pcell_borrow_mut 

Source 
pub exec fn pcell_borrow_mut<'a, T>(
    cell: &'a PCell<T>,
    perm: &'a mut Tracked<PointsTo<T>>,
) -> res : &'a mut T
Expand description
requires
cell.id() == perm.id(),
ensures
*final(res) == *final(perm).value(),
final(perm).id() == old(perm).id(),

A Verus version of unsafe { &mut *cell.get() } for UnsafeCell<T>. FIXME: Waiting for official support from Verus.