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(points_to): Tracked<&'a PointsTo<MetaSlot>>,
    Tracked(slot_owner): Tracked<&'a mut MetaSlotOwner>,
    Tracked(repr_perm): Tracked<&'a mut M::ReprPerm>,
) -> res : &'a mut M
Expand description
requires
old(slot_owner).inv(),
points_to.value().wf(*old(slot_owner)),
typed_meta_wf::<M>(*points_to, old(slot_owner).metadata_perm, *old(repr_perm)),
ptr.addr() == points_to.addr(),
ensures
*res == typed_meta_value::<M>(old(slot_owner).metadata_perm, *old(repr_perm)),
final(slot_owner).inv(),
points_to.value().wf(*final(slot_owner)),
final(slot_owner).slot_vaddr == old(slot_owner).slot_vaddr,
final(slot_owner).usage == old(slot_owner).usage,
final(slot_owner).paths_in_pt == old(slot_owner).paths_in_pt,
final(slot_owner).ref_count_perm == old(slot_owner).ref_count_perm,
final(slot_owner).vtable_ptr_perm() == old(slot_owner).vtable_ptr_perm(),
final(slot_owner).in_list_perm == old(slot_owner).in_list_perm,
typed_meta_wf::<M>(*points_to, final(slot_owner).metadata_perm, *final(repr_perm)),
*final(res) == typed_meta_value::<M>(final(slot_owner).metadata_perm, *final(repr_perm)),