Skip to main content

vaddr_range_spec

ostd::mm::page_table

Function vaddr_range_spec 

Source 
pub open spec fn vaddr_range_spec<C: PageTableConfig>() -> Range<Vaddr>
Expand description
{
    let idx_range = C::TOP_LEVEL_INDEX_RANGE_spec();
    let offset = pte_index_bit_offset::<C::C>(C::NR_LEVELS()) as nat;
    let start = idx_range.start * pow2(offset);
    let end_inclusive = idx_range.end * pow2(offset) - 1;
    (start as Vaddr)..((end_inclusive + 1) as Vaddr)
}

Spec for the managed virtual address range (exclusive end). For configs without VA_SIGN_EXT (e.g. UserPtConfig) or when the base range has sign bit 0. Configs with sign extension (e.g. KernelPtConfig) use vaddr_range_bounds_spec for their canonical high-half bounds.