paddr_to_vaddr

ostd::specs::arch

Function paddr_to_vaddr 

Source 
pub exec fn paddr_to_vaddr(pa: Paddr) -> res : usize
Expand description
requires
pa < VMALLOC_BASE_VADDR() - LINEAR_MAPPING_BASE_VADDR(),
ensures
res == paddr_to_vaddr_spec(pa),