get_slot

ostd::mm::frame::meta

Function get_slot 

Source 
pub exec fn get_slot(
    paddr: Paddr,
    verus_tmp_owner: Tracked<&MetaSlotOwner>,
) -> res : Result<PPtr<MetaSlot>, GetFrameError>
Expand description
requires
owner.self_addr == frame_to_meta(paddr),
owner.inv(),
ensures
res.is_ok() ==> res.unwrap().addr() == frame_to_meta(paddr),

Gets the reference to a metadata slot.