Skip to main content

valid_slot_vaddr

ostd::specs::mm::frame::frame_specs

Function valid_slot_vaddr 

Source 
pub open spec fn valid_slot_vaddr(addr: Vaddr) -> bool
Expand description
{
    &&& valid_frame_paddr(meta_to_frame(addr))
    &&& addr % META_SLOT_SIZE == 0
    &&& FRAME_METADATA_RANGE.start <= addr
        < FRAME_METADATA_RANGE.start + MAX_NR_PAGES * META_SLOT_SIZE

}