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 }