Enum MappedItem 

pub enum MappedItem {
    Tracked(DynFrame, PageProperty),
    Untracked(Paddr, PagingLevel, PageProperty),
}

Variants

Tracked(DynFrame, PageProperty)

Untracked(Paddr, PagingLevel, PageProperty)

Implementations

impl MappedItem

pub fn arrow_2(self) -> PageProperty

pub fn arrow_Tracked_0(self) -> DynFrame

pub fn arrow_Tracked_1(self) -> PageProperty

pub fn arrow_Untracked_0(self) -> Paddr

pub fn arrow_Untracked_1(self) -> PagingLevel

pub fn arrow_Untracked_2(self) -> PageProperty

Trait Implementations

impl RCClone for MappedItem

open spec fn clone_requires(self, perm: MetaRegionOwners) -> bool

{
    match self {
        MappedItem::Tracked(frame, _) => frame.clone_requires(perm),
        MappedItem::Untracked(_, _, _) => perm.inv(),
    }
}

open spec fn clone_ensures( self, old_perm: MetaRegionOwners, new_perm: MetaRegionOwners, res: Self, ) -> bool

{
    match (self, res) {
        (MappedItem::Tracked(frame, prop), MappedItem::Tracked(res_frame, res_prop)) => (
            &&& prop == res_prop
            &&& frame.clone_ensures(old_perm, new_perm, res_frame)

        ),
        (
            MappedItem::Untracked(pa, level, prop),
            MappedItem::Untracked(res_pa, res_level, res_prop),
        ) => (
            &&& pa == res_pa
            &&& level == res_level
            &&& prop == res_prop
            &&& old_perm == new_perm

        ),
        _ => false,
    }
}

exec fn clone(&self, Tracked(perm): Tracked<&mut MetaRegionOwners>) -> res : Self