VmIoOnce

ostd::mm::io

Trait VmIoOnce 

Source 
pub trait VmIoOnce: Sized {
    // Required methods
    spec fn obeys_vmio_once_read_requires() -> bool;
    spec fn obeys_vmio_once_write_requires() -> bool;
    spec fn obeys_vmio_once_read_ensures() -> bool;
    spec fn obeys_vmio_once_write_ensures() -> bool;
    exec fn read_once<T: PodOnce>(&self, offset: usize) -> Result<T, Error>;
    exec fn write_once<T: PodOnce>(
        &self,
        offset: usize,
        new_val: &T,
    ) -> Result<(), Error>;
}
Expand description

A trait that enables reading/writing data from/to a VM object using one non-tearing memory load/store.

See also VmIo, which enables reading/writing data from/to a VM object without the guarantee of using one non-tearing memory load/store.

Required Methods§

Source

spec fn obeys_vmio_once_read_requires() -> bool

Source

spec fn obeys_vmio_once_write_requires() -> bool

Source

spec fn obeys_vmio_once_read_ensures() -> bool

Source

spec fn obeys_vmio_once_write_ensures() -> bool

Source

exec fn read_once<T: PodOnce>(&self, offset: usize) -> Result<T, Error>

Reads a value of the PodOnce type at the specified offset using one non-tearing memory load.

Except that the offset is specified explicitly, the semantics of this method is the same as [VmReader::read_once].

Source

exec fn write_once<T: PodOnce>( &self, offset: usize, new_val: &T, ) -> Result<(), Error>

Writes a value of the PodOnce type at the specified offset using one non-tearing memory store.

Except that the offset is specified explicitly, the semantics of this method is the same as VmWriter::write_once.

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§