Function load_pte

pub exec fn load_pte<E: PageTableEntryTrait>(
    ptr: ArrayPtr<E, CONST_NR_ENTRIES>,
    ordering: Ordering,
) -> pte : E

Expand description

with

Tracked(perm): Tracked <& vstd_extra ::array_ptr ::PointsTo <E,CONST_NR_ENTRIES>>,

requires

perm.is_init(ptr.index as int),

perm.addr() == ptr.addr(),

ensures

pte == perm.value()[ptr.index as int],

Loads a page table entry with an atomic instruction.

§Safety

The safety preconditions are same as those of AtomicUsize::from_ptr.