Enum Type

pub enum Type {
    BitVector(Option<usize>),
    Bool,
    Int,
    Unit,
}

Verification type

Variants

BitVector(Option<usize>)

The expression is a bitvector, currently modeled in the logic QF_BV https://SMT-LIB.cs.uiowa.edu/version1/logics/QF_BV.smt This corresponds to Cranelift’s Isle type: (type Value (primitive Value))

Bool

The expression is a boolean. This does not directly correspond to a specific Cranelift Isle type, rather, we use it for the language of assertions.

Int

The expression is an Isle type. This is separate from BitVector because it allows us to use a different solver type (e.h., Int) This corresponds to Cranelift’s Isle type: (type Type (primitive Type))

Unit

Trait Implementations

impl Clone for Type

fn clone(&self) -> Type

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Type

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

Formats the value using the given formatter.

impl Display for Type

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

Formats the value using the given formatter.

impl Hash for Type

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for Type

fn eq(&self, other: &Type) -> 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 Type

impl Eq for Type

impl StructuralPartialEq for Type