Struct PageProperty 

pub struct PageProperty {
    pub flags: PageFlags,
    pub cache: CachePolicy,
    pub priv_flags: PrivilegedPageFlags,
}

The property of a mapped virtual memory page.

Fields

flags: PageFlags

The flags associated with the page,

cache: CachePolicy

The cache policy for the page.

priv_flags: PrivilegedPageFlags

Implementations

impl PageProperty

pub exec fn new_user(flags: PageFlags, cache: CachePolicy) -> Self

returns

Self::new_user(flags, cache),

Creates a new PageProperty with the given flags and cache policy for the user.

pub fn __VERUS_SPEC_new_user(flags: PageFlags, cache: CachePolicy) -> Self

pub exec fn new_absent() -> Self

returns

Self::new_absent(),

Creates a page property that implies an invalid page without mappings.

pub fn __VERUS_SPEC_new_absent() -> Self

impl PageProperty

pub proof fn lemma_avail1_tag_encoding(self)

ensures

self.flags.union(PageFlags::AVAIL1()).contains(PageFlags::AVAIL1()),

!self.flags.difference(PageFlags::AVAIL1()).contains(PageFlags::AVAIL1()),

!self.flags.contains(PageFlags::AVAIL1())
    ==> self.flags.difference(PageFlags::AVAIL1()) == self.flags,

!self.flags.contains(PageFlags::AVAIL1())
    ==> self.flags.union(PageFlags::AVAIL1()).difference(PageFlags::AVAIL1())
        == self.flags,

self.flags.contains(PageFlags::AVAIL1())
    ==> self.flags.difference(PageFlags::AVAIL1()).union(PageFlags::AVAIL1())
        == self.flags,

Adding and removing AVAIL1 is reversible when it is used as a reserved tag.

Trait Implementations

impl Clone for PageProperty

fn clone(&self) -> PageProperty

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for PageProperty

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

Formats the value using the given formatter.

impl Inv for PageProperty

open spec fn inv(self) -> bool

{
    &&& self.flags.bits() & PageFlags::all().bits() == self.flags.bits()
    &&& self.priv_flags.bits() & PrivilegedPageFlags::all().bits()
        == self.priv_flags.bits()

}

impl PartialEq for PageProperty

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

Tests for self and other values to be equal, and is used by ==.

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

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

impl Copy for PageProperty

impl Eq for PageProperty

impl StructuralPartialEq for PageProperty