paddr_to_vaddr_spec

ostd::specs::arch::kspace

Function paddr_to_vaddr_spec 

Source 
pub open spec fn paddr_to_vaddr_spec(pa: Paddr) -> usize
Expand description
recommends
pa < VMALLOC_BASE_VADDR() - LINEAR_MAPPING_BASE_VADDR(),
{ (pa + LINEAR_MAPPING_BASE_VADDR()) as usize }