Skip to main content

MappedItem

ostd::mm::kspace

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, _), MappedItem::Tracked(res_frame, _)) => {
            frame.clone_ensures(old_perm, new_perm, res_frame)
        }
        (MappedItem::Untracked(_, _, _), _) => old_perm == new_perm,
        _ => true,
    }
}

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

Auto Trait Implementations§

impl Freeze for MappedItem

impl !RefUnwindSafe for MappedItem

impl Send for MappedItem

impl Sync for MappedItem

impl Unpin for MappedItem

impl UnsafeUnpin for MappedItem

impl UnwindSafe for MappedItem

Blanket Implementations§

impl<T> Any for T
where T: 'static + ?Sized,

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more

impl<T> Borrow<T> for T
where T: ?Sized,

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more

impl<T> BorrowMut<T> for T
where T: ?Sized,

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more

impl<T> From<T> for T

fn from(t: T) -> T

Returns the argument unchanged.

impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: From<T>,

fn obeys_from_spec() -> bool

fn from_spec(v: T) -> VERUS_SPEC__A

impl<T, U> Into<U> for T
where U: From<T>,

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: Into<T>,

fn obeys_into_spec() -> bool

fn into_spec(self) -> T

impl<T, U> IntoSpecImpl<U> for T
where U: From<T>,

fn obeys_into_spec() -> bool

fn into_spec(self) -> U

impl<T, U> TryFrom<U> for T
where U: Into<T>,

type Error = Infallible

The type returned in the event of a conversion error.

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryFrom<T>,

fn obeys_try_from_spec() -> bool

fn try_from_spec( v: T, ) -> Result<VERUS_SPEC__A, <VERUS_SPEC__A as TryFrom<T>>::Error>

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

fn obeys_try_into_spec() -> bool

fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

impl<T, U> TryIntoSpecImpl<U> for T
where U: TryFrom<T>,

fn obeys_try_into_spec() -> bool

fn try_into_spec(self) -> Result<U, <U as TryFrom<T>>::Error>