Skip to main content

FrameContents

ostd::specs::mm::virt_mem_newer

Struct FrameContents

pub struct FrameContents {
    pub contents: Seq<MemContents<u8>>,
    pub size: usize,
    pub range: Range<Paddr>,
}

Expand description

Byte contents of one physical frame range tracked in a MemView.

This is the physical-memory side of the model: each frame base Paddr maps to a FrameContents value whose metadata (size, range) constrains how contents can be interpreted.

Fields§

§contents: Seq<MemContents<u8>>

Per-byte initialization/value state for this frame.

§size: usize

Frame size in bytes.

§range: Range<Paddr>

Physical range covered by this frame, modeled as [start, end).

Trait Implementations§

impl Inv for FrameContents

open spec fn inv(self) -> bool

{
    &&& self.contents.len() == self.size@
    &&& self.size@ == self.range.end - self.range.start
    &&& self.range.start % self.size == 0
    &&& self.range.end % self.size == 0
    &&& self.range.start <= self.range.end < MAX_PADDR

}

Well-formedness invariant for FrameContents.

§Invariant

contents.len() == size.
size == range.end - range.start.
range.start and range.end are aligned to size.
range is ordered and remains below MAX_PADDR.

Auto Trait Implementations§

impl Freeze for FrameContents

impl RefUnwindSafe for FrameContents

impl Send for FrameContents

impl Sync for FrameContents

impl Unpin for FrameContents

impl UnsafeUnpin for FrameContents

impl UnwindSafe for FrameContents

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>