vaddr_to_paddr

ostd::specs::arch::kspace

Function vaddr_to_paddr 

Source 
pub exec fn vaddr_to_paddr(va: Vaddr) -> res : usize
Expand description
requires
LINEAR_MAPPING_BASE_VADDR() <= va < VMALLOC_BASE_VADDR(),
ensures
res == vaddr_to_paddr(va),