Skip to main content

is_mmio_paddr

ostd::specs::mm::frame::meta_owners

Function is_mmio_paddr 

Source 
pub uninterp fn is_mmio_paddr(pa: Paddr) -> bool
Expand description

Whether pa falls in an MMIO physical-address range. Uninterpreted at the spec level — concrete arch- and machine-specific MMIO range layouts are outside the verification surface, but the kernel allocator (which picks slots with PageUsage::Unused) is guaranteed disjoint from MMIO mappings.