Skip to main content

vaddr_at

ostd::specs::mm::page_table

Function vaddr_at 

Source 
pub open spec fn vaddr_at(path: TreePath<NR_ENTRIES>, leading_bits: int) -> usize
Expand description
{ (vaddr(path) as int + leading_bits * 0x1_0000_0000_0000int) as usize }

Virtual address of path with leading_bits placed in bits [48, 64).

Matches AbstractVaddr { offset: 0, index: <from path>, leading_bits } .to_vaddr() modulo the offset. For leading_bits == 0 this reduces to vaddr(path); for leading_bits == 0xffff and a kernel path this yields the canonical sign-extended high-half address.