Enum move_ir_types::spec_language_ast::SpecExp

pub enum SpecExp {
    Constant(CopyableVal_),
    StorageLocation(StorageLocation),
    GlobalExists {
        type_: QualifiedStructIdent,
        type_actuals: Vec<Type>,
        address: StorageLocation,
    },
    Dereference(StorageLocation),
    Reference(StorageLocation),
    Not(Box<SpecExp>),
    Binop(Box<SpecExp>, BinOp, Box<SpecExp>),
    Update(Box<SpecExp>, Box<SpecExp>),
    Old(Box<SpecExp>),
    Call(Symbol, Vec<SpecExp>),
}

An expression in the specification language

Variants

Constant(CopyableVal_)

A Move constant

StorageLocation(StorageLocation)

A spec language storage location

GlobalExists

Fields

type_: QualifiedStructIdent

type_actuals: Vec<Type>

address: StorageLocation

Lifting the Move exists operator to a storage location

Dereference(StorageLocation)

Dereference of a storage location (written *s)

Reference(StorageLocation)

Reference to a storage location (written &s)

Not(Box<SpecExp>)

Negation of a boolean expression (written !e),

Binop(Box<SpecExp>, BinOp, Box<SpecExp>)

Binary operators also suported by Move

Update(Box<SpecExp>, Box<SpecExp>)

Update expr (i := 1 inside [])

Old(Box<SpecExp>)

Value of expression evaluated in the state before function enter.

Call(Symbol, Vec<SpecExp>)

Call to a helper function.

Trait Implementations

impl Clone for SpecExp

fn clone(&self) -> SpecExp

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for SpecExp

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

Formats the value using the given formatter.

impl PartialEq<SpecExp> for SpecExp

fn eq(&self, other: &SpecExp) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

This method tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for SpecExp