Skip to main content

vaddr_of

ostd::specs::mm::page_table

Function vaddr_of 

Source 
pub open spec fn vaddr_of<C: PageTableConfig>(path: TreePath<NR_ENTRIES>) -> usize
Expand description
{ vaddr_at(path, C::LEADING_BITS_spec() as int) }

Config-aware vaddr: reads leading_bits from C::LEADING_BITS_spec().

Every Mapping produced by a cursor on PageTable<C> should be built with this — not the bare vaddr(path) — so the VA lives in the range advertised by C::VADDR_RANGE_spec().