has_safe_slot

ostd::mm::frame::meta

Function has_safe_slot 

Source 
pub open spec fn has_safe_slot(paddr: Paddr) -> bool
Expand description
{
    &&& paddr % PAGE_SIZE == 0
    &&& paddr < MAX_PADDR

}