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 }