kvirt_alloc_range_bounds

ostd::mm::kspace::kvirt_area

Function kvirt_alloc_range_bounds 

Source 
pub proof fn kvirt_alloc_range_bounds(
    area_size: usize,
    map_offset: usize,
    r: Range<Vaddr>,
)
Expand description
ensures
kvirt_alloc_spec(area_size) == Ok::<core::ops::Range<Vaddr>, RangeAllocError>(r)
    ==> r.start <= r.end && (r.end - r.start) >= area_size
        && map_offset <= r.end - r.start && r.start + map_offset <= usize::MAX
        && r.start % PAGE_SIZE == 0 && r.end % PAGE_SIZE == 0
        && KERNEL_BASE_VADDR <= r.start && r.end <= KERNEL_END_VADDR,