vaddr_to_paddr_spec

ostd::specs::arch

Function vaddr_to_paddr_spec 

Source 
pub open spec fn vaddr_to_paddr_spec(va: Vaddr) -> usize
Expand description
recommends
LINEAR_MAPPING_BASE_VADDR <= va < VMALLOC_BASE_VADDR,
{ (va - LINEAR_MAPPING_BASE_VADDR) as usize }