Trait Plain 

pub trait Plain: Copy {
    // Required method
    fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self>;
}

A trait for types that can be extracted from snapshots in ghost code.

These are types that only contain plain data and whose ownership does not convey any additional information.

For example, Booleans and integers are plain, but references are not, be they mutable or not. Indeed, the ownership of a shared reference can be used to deduce facts, for example with Perm::disjoint_lemma.

Required Methods

fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self>

ensures

*result == *snap

terminates

ghost

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.

Implementations on Foreign Types

impl Plain for bool

fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self>

ensures

*result == *snap

terminates

ghost

impl Plain for char

fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self>

ensures

*result == *snap

terminates

ghost

impl Plain for i8

fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self>

ensures

*result == *snap

terminates

ghost

impl Plain for i16

fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self>

ensures

*result == *snap

terminates

ghost

impl Plain for i32

fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self>

ensures

*result == *snap

terminates

ghost

impl Plain for i64

fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self>

ensures

*result == *snap

terminates

ghost

impl Plain for i128

fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self>

ensures

*result == *snap

terminates

ghost

impl Plain for isize

fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self>

ensures

*result == *snap

terminates

ghost

impl Plain for u8

fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self>

ensures

*result == *snap

terminates

ghost

impl Plain for u16

fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self>

ensures

*result == *snap

terminates

ghost

impl Plain for u32

fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self>

ensures

*result == *snap

terminates

ghost

impl Plain for u64

fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self>

ensures

*result == *snap

terminates

ghost

impl Plain for u128

fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self>

ensures

*result == *snap

terminates

ghost

impl Plain for usize

fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self>

ensures

*result == *snap

terminates

ghost

impl<T> Plain for *const T

fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self>

ensures

*result == *snap

terminates

ghost

impl<T> Plain for *mut T

fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self>

ensures

*result == *snap

terminates

ghost

Implementors

impl Plain for Id

impl Plain for Int

impl Plain for Namespace

impl<T: Plain> Plain for Seq<T>