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_owner(paddr);
    &&& regions.contains(frame_to_index(paddr))
    &&& so.ref_count() > 0
    &&& so.ref_count() != REF_COUNT_UNUSED
    &&& so.ref_count() <= REF_COUNT_MAX
    &&& so.ref_count() == 1
        ==> {
            &&& so.storage_perm().is_init()
            &&& so.in_list_perm.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.