is_valid_range_spec

ostd::mm::page_table

Function is_valid_range_spec 

Source 
pub open spec fn is_valid_range_spec<C: PageTableConfig>(r: &Range<Vaddr>) -> bool
Expand description
{
    let va_range = vaddr_range_spec::<C>();
    (r.start == 0 && r.end == 0)
        || (va_range.start <= r.start && r.end > 0 && r.end - 1 <= va_range.end - 1)
}

Spec for whether a range is within the page table’s managed address space.