Skip to main content

drop_pre

ostd::specs::mm::embedding::frame

Function drop_pre 

Source 
pub open spec fn drop_pre(regions: MetaRegionOwners, paddr: Paddr) -> bool
Expand description
{
    let so = regions.slot_owners[frame_to_index(paddr)];
    &&& regions.slots.contains_key(frame_to_index(paddr))
    &&& so.inner_perms.ref_count.value() > 0
    &&& so.inner_perms.ref_count.value() != REF_COUNT_UNUSED
    &&& so.inner_perms.ref_count.value() <= REF_COUNT_MAX
    &&& so.inner_perms.ref_count.value() == 1
        ==> {
            &&& so.inner_perms.storage.is_init()
            &&& so.inner_perms.in_list.value() == 0
            &&& so.paths_in_pt.is_empty()

        }

}

Op::FrameDrop precondition over the slot at paddr. Mirrors Frame::drop_requires (expressible parts) verbatim — no extra embedding obligation. There is no caller-visible decrement-vs-teardown choice — the single frame_drop_embedded axiom covers both via one postcondition keyed on the live refcount.