Skip to main content

MetaSlotModel

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

Struct MetaSlotModel

pub struct MetaSlotModel {
    pub status: MetaSlotStatus,
    pub storage: MemContents<MetaSlotStorage>,
    pub ref_count: u64,
    pub vtable_ptr: MemContents<usize>,
    pub in_list: u64,
    pub self_addr: usize,
    pub usage: PageUsage,
}

Fields§

§status: MetaSlotStatus§storage: MemContents<MetaSlotStorage>§ref_count: u64§vtable_ptr: MemContents<usize>§in_list: u64§self_addr: usize§usage: PageUsage

Trait Implementations§

impl Inv for MetaSlotModel

open spec fn inv(self) -> bool

{
    match self.ref_count {
        REF_COUNT_UNUSED => (
            &&& self.vtable_ptr.is_uninit()
            &&& self.in_list == 0

        ),
        REF_COUNT_UNIQUE => (
            &&& self.vtable_ptr.is_init()

        ),
        0 => (
            &&& self.in_list == 0

        ),
        _ if self.ref_count < REF_COUNT_MAX => (
            &&& self.vtable_ptr.is_init()

        ),
        _ => false,
    }
}

Auto Trait Implementations§

impl !Freeze for MetaSlotModel

impl !RefUnwindSafe for MetaSlotModel

impl Send for MetaSlotModel

impl Sync for MetaSlotModel

impl Unpin for MetaSlotModel

impl UnsafeUnpin for MetaSlotModel

impl UnwindSafe for MetaSlotModel

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>