MemoryRegion

ostd::boot::memory_region

Struct MemoryRegion 

Source 
pub struct MemoryRegion { /* private fields */ }
Expand description

The information of initial memory regions that are needed by the kernel. The sections are not guaranteed to not overlap. The region must be page aligned.

Implementations§

Source§

impl MemoryRegion

Source

pub const exec fn new(base: Paddr, len: usize, typ: MemoryRegionType) -> ret : Self

requires
base + len <= MAX_PADDR(),
ensures
ret.inv(),
ret@
    == (MemRegionModel {
        base: base as int,
        end: base + len,
        typ: typ.to_int(),
    }),

Constructs a valid memory region.

Source

pub const exec fn VERUS_UNERASED_PROXY__new( base: Paddr, len: usize, typ: MemoryRegionType, ) -> ret : Self

requires
base + len <= MAX_PADDR(),
ensures
ret.inv(),
ret@
    == (MemRegionModel {
        base: base as int,
        end: base + len,
        typ: typ.to_int(),
    }),

Constructs a valid memory region.

Source

pub const exec fn bad() -> ret : Self

ensures
ret.inv(),
ret@ == MemRegionModel::bad(),

Constructs a bad memory region.

Source

pub const exec fn VERUS_UNERASED_PROXY__bad() -> ret : Self

ensures
ret.inv(),
ret@ == MemRegionModel::bad(),

Constructs a bad memory region.

Source

pub fn base(&self) -> Paddr

The physical address of the base of the region.

Source

pub fn __VERUS_SPEC_base(&self) -> Paddr

Source

pub fn len(&self) -> usize

The length in bytes of the region.

Source

pub fn __VERUS_SPEC_len(&self) -> usize

Source

pub exec fn end(&self) -> Paddr

requires
self.inv(),

The physical address of the end of the region.

Source

pub fn __VERUS_SPEC_end(&self) -> Paddr

Source

pub fn is_empty(&self) -> bool

Checks whether the region is empty

Source

pub fn __VERUS_SPEC_is_empty(&self) -> bool

Source

pub fn typ(&self) -> MemoryRegionType

The type of the region.

Source

pub fn __VERUS_SPEC_typ(&self) -> MemoryRegionType

Trait Implementations§

Source§

impl Clone for MemoryRegion

Source§

fn clone(&self) -> MemoryRegion

Returns a duplicate of the value. Read more
1.0.0 · Source§

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source. Read more
Source§

impl Debug for MemoryRegion

Source§

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter. Read more
Source§

impl Inv for MemoryRegion

Source§

closed spec fn inv(self) -> bool

Source§

impl InvView for MemoryRegion

Source§

proof fn view_preserves_inv(self)

Source§

impl Ord for MemoryRegion

Source§

fn cmp(&self, other: &MemoryRegion) -> Ordering

This method returns an Ordering between self and other. Read more
1.21.0 · Source§

fn max(self, other: Self) -> Self
where Self: Sized,

Compares and returns the maximum of two values. Read more
1.21.0 · Source§

fn min(self, other: Self) -> Self
where Self: Sized,

Compares and returns the minimum of two values. Read more
1.50.0 · Source§

fn clamp(self, min: Self, max: Self) -> Self
where Self: Sized,

Restrict a value to a certain interval. Read more
Source§

impl PartialEq for MemoryRegion

Source§

fn eq(&self, other: &MemoryRegion) -> bool

Tests for self and other values to be equal, and is used by ==.
1.0.0 · Source§

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.
Source§

impl PartialOrd for MemoryRegion

Source§

fn partial_cmp(&self, other: &MemoryRegion) -> Option<Ordering>

This method returns an ordering between self and other values if one exists. Read more
1.0.0 · Source§

fn lt(&self, other: &Rhs) -> bool

Tests less than (for self and other) and is used by the < operator. Read more
1.0.0 · Source§

fn le(&self, other: &Rhs) -> bool

Tests less than or equal to (for self and other) and is used by the <= operator. Read more
1.0.0 · Source§

fn gt(&self, other: &Rhs) -> bool

Tests greater than (for self and other) and is used by the > operator. Read more
1.0.0 · Source§

fn ge(&self, other: &Rhs) -> bool

Tests greater than or equal to (for self and other) and is used by the >= operator. Read more
Source§

impl View for MemoryRegion

Source§

closed spec fn view(&self) -> Self::V

Source§

type V = MemRegionModel

Source§

impl Copy for MemoryRegion

Source§

impl Eq for MemoryRegion

Source§

impl StructuralPartialEq for MemoryRegion

Auto Trait Implementations§

Blanket Implementations§

Source§

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

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

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

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

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

Source§

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

Mutably borrows from an owned value. Read more
Source§

impl<T> CloneToUninit for T
where T: Clone,

Source§

unsafe fn clone_to_uninit(&self, dest: *mut u8)

🔬This is a nightly-only experimental API. (clone_to_uninit)
Performs copy-assignment from self to dest. Read more
Source§

impl<T> From<T> for T

Source§

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

Source§

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

Source§

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<VERUS_SPEC__A> OrdSpec for VERUS_SPEC__A
where VERUS_SPEC__A: Ord + ?Sized,

§

fn obeys_cmp_spec() -> bool

§

fn cmp_spec(&self, other: &VERUS_SPEC__A) -> Ordering

§

impl<A, Rhs> PartialEqIs<Rhs> for A
where A: PartialEq<Rhs> + ?Sized, Rhs: ?Sized,

§

fn is_eq(&self, other: &Rhs) -> bool

§

fn is_ne(&self, other: &Rhs) -> bool

§

impl<Rhs, VERUS_SPEC__A> PartialEqSpec<Rhs> for VERUS_SPEC__A
where VERUS_SPEC__A: PartialEq<Rhs> + ?Sized, Rhs: ?Sized,

§

fn obeys_eq_spec() -> bool

§

fn eq_spec(&self, other: &Rhs) -> bool

§

impl<A, Rhs> PartialOrdIs<Rhs> for A
where A: PartialOrd<Rhs> + ?Sized, Rhs: ?Sized,

§

fn is_lt(&self, other: &Rhs) -> bool

§

fn is_le(&self, other: &Rhs) -> bool

§

fn is_gt(&self, other: &Rhs) -> bool

§

fn is_ge(&self, other: &Rhs) -> bool

§

impl<Rhs, VERUS_SPEC__A> PartialOrdSpec<Rhs> for VERUS_SPEC__A
where VERUS_SPEC__A: PartialOrd<Rhs> + ?Sized, Rhs: ?Sized,

§

fn obeys_partial_cmp_spec() -> bool

§

fn partial_cmp_spec(&self, other: &Rhs) -> Option<Ordering>

Source§

impl<T> ToOwned for T
where T: Clone,

Source§

type Owned = T

The resulting type after obtaining ownership.
Source§

fn to_owned(&self) -> T

Creates owned data from borrowed data, usually by cloning. Read more
Source§

fn clone_into(&self, target: &mut T)

Uses borrowed data to replace owned data, usually by cloning. Read more
Source§

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

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

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>

Source§

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

Source§

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

The type returned in the event of a conversion error.
Source§

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>