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),