Trait ExecSpecMemContents 

pub trait ExecSpecMemContents<'a>: Sized + DeepView {
    type Elem: DeepView + DeepViewClone;

    // Required methods
    spec fn is_init_spec(&self) -> bool;
    exec fn exec_is_init(self) -> bool;
    exec fn exec_is_uninit(self) -> bool;
    exec fn exec_value(self) -> Self::Elem;
}

Traits for MemContents methods Spec for executable versions of MemContents::is_init, MemContents::is_uninit, and MemContents::value.

Required Associated Types

type Elem: DeepView + DeepViewClone

Required Methods

spec fn is_init_spec(&self) -> bool

exec fn exec_is_init(self) -> bool

exec fn exec_is_uninit(self) -> bool

exec fn exec_value(self) -> Self::Elem

requires

self.is_init_spec(),

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors

impl<'a, T> ExecSpecMemContents<'a> for &'a ExecMemContents<T>

where T: DeepView + DeepViewClone,

Impls for MemContents methods

type Elem = T