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_spec::<C::C>(C::NR_LEVELS()) as nat;
    let start = (idx_range.start as int) * pow2(offset);
    let end_inclusive = (idx_range.end as int) * 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 a wrapped range in exec; we use an axiom to connect that case.