Skip to main content

borrow_meta_mut

ostd::specs::mm::frame::meta_owners

Function borrow_meta_mut 

Source 
pub exec fn borrow_meta_mut<'a, M: AnyFrameMeta + Repr<MetaSlotStorage>>(
    ptr: ReprPtr<MetaSlotStorage, M>,
    Tracked(slot_perm): Tracked<&'a PointsTo<MetaSlot>>,
    Tracked(metadata_perms): Tracked<&'a mut MetadataPerm>,
    Tracked(repr_perm): Tracked<&'a mut M::ReprPerm>,
) -> res : &'a mut M
Expand description
requires
ptr.addr() == slot_perm.addr(),
typed_meta_wf::<M>(*slot_perm, *old(metadata_perms), *old(repr_perm)),
ensures
*res == typed_meta_value::<M>(*old(metadata_perms), *old(repr_perm)),
*final(res) == typed_meta_value::<M>(*final(metadata_perms), *final(repr_perm)),
typed_meta_wf::<M>(*slot_perm, *final(metadata_perms), *final(repr_perm)),