Enum Val 

pub enum Val<B> {
    Symbolic(Sym),
    I64(i64),
    I128(i128),
    Bool(bool),
    Bits(B),
    String(String),
    Unit,
    Vector(Vec<Val<B>>),
    List(Vec<Val<B>>),
    Enum(EnumMember),
    Struct(HashMap<Name, Val<B>>),
    Ctor(Name, Box<Val<B>>),
    Ref(Name),
    Poison,
}

A value is either a symbolic value, represented as Symbolic(n) for where n is the identifier of the variable in the SMT solver, or one of the concrete values in this enum.

Variants

Symbolic(Sym)

I64(i64)

I128(i128)

Bool(bool)

Bits(B)

String(String)

Unit

Vector(Vec<Val<B>>)

List(Vec<Val<B>>)

Enum(EnumMember)

Struct(HashMap<Name, Val<B>>)

Ctor(Name, Box<Val<B>>)

Ref(Name)

Poison

Implementations

impl<B: BV> Val<B>

pub fn symbolic_variables(&self) -> HashSet<Sym>

pub fn is_symbolic(&self) -> bool

pub fn as_bits(&self) -> Option<&B>

pub fn to_string(&self, symtab: &Symtab<'_>) -> String

pub fn plausible<N: Debug>( &self, ty: &Ty<N>, symtab: &Symtab<'_>, ) -> Result<(), String>

Just enough of a type check to pick up bad default registers

Trait Implementations

impl<B: Clone> Clone for Val<B>

fn clone(&self) -> Val<B>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<B: Debug> Debug for Val<B>

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

Formats the value using the given formatter.