frame_entry_wf

ostd::mm::kspace::kvirt_area

Function frame_entry_wf 

Source 
pub open spec fn frame_entry_wf<T: AnyFrameMeta>(
    frame: Frame<T>,
    prop: PageProperty,
    entry_owner: EntryOwner<KernelPtConfig>,
) -> bool
Expand description
{
    let frame_mss = DynFrame {
        ptr: frame.ptr,
        _marker: PhantomData,
    };
    let item = MappedItem::Tracked(frame_mss, prop);
    let (pa, level, prop_from_item) = KernelPtConfig::item_into_raw_spec(item);
    Child::Frame(pa, level, prop_from_item).wf(entry_owner)
}

Spec function: the entry owner correctly matches the frame and property for mapping.