Enum move_model::ast::Operation
source · pub enum Operation {
Show 62 variants
Function(ModuleId, SpecFunId, Option<Vec<MemoryLabel>>),
Pack(ModuleId, StructId),
Tuple,
Select(ModuleId, StructId, FieldId),
UpdateField(ModuleId, StructId, FieldId),
Result(usize),
Index,
Slice,
Range,
Add,
Sub,
Mul,
Mod,
Div,
BitOr,
BitAnd,
Xor,
Shl,
Shr,
Implies,
Iff,
And,
Or,
Eq,
Identical,
Neq,
Lt,
Gt,
Le,
Ge,
Not,
Len,
TypeValue,
TypeDomain,
ResourceDomain,
Global(Option<MemoryLabel>),
Exists(Option<MemoryLabel>),
CanModify,
Old,
Trace,
EmptyVec,
SingleVec,
UpdateVec,
ConcatVec,
IndexOfVec,
ContainsVec,
InRangeRange,
InRangeVec,
RangeVec,
MaxU8,
MaxU64,
MaxU128,
AbortFlag,
AbortCode,
WellFormed,
BoxValue,
UnboxValue,
EmptyEventStore,
ExtendEventStore,
EventStoreIncludes,
EventStoreIncludedIn,
NoOp,
}
Variants§
Function(ModuleId, SpecFunId, Option<Vec<MemoryLabel>>)
Pack(ModuleId, StructId)
Tuple
Select(ModuleId, StructId, FieldId)
UpdateField(ModuleId, StructId, FieldId)
Result(usize)
Index
Slice
Range
Add
Sub
Mul
Mod
Div
BitOr
BitAnd
Xor
Shl
Shr
Implies
Iff
And
Or
Eq
Identical
Neq
Lt
Gt
Le
Ge
Not
Len
TypeValue
TypeDomain
ResourceDomain
Global(Option<MemoryLabel>)
Exists(Option<MemoryLabel>)
CanModify
Old
Trace
EmptyVec
SingleVec
UpdateVec
ConcatVec
IndexOfVec
ContainsVec
InRangeRange
InRangeVec
RangeVec
MaxU8
MaxU64
MaxU128
AbortFlag
AbortCode
WellFormed
BoxValue
UnboxValue
EmptyEventStore
ExtendEventStore
EventStoreIncludes
EventStoreIncludedIn
NoOp
Implementations§
Trait Implementations§
source§impl PartialEq<Operation> for Operation
impl PartialEq<Operation> for Operation
impl Eq for Operation
impl StructuralEq for Operation
impl StructuralPartialEq for Operation
Auto Trait Implementations§
impl RefUnwindSafe for Operation
impl Send for Operation
impl Sync for Operation
impl Unpin for Operation
impl UnwindSafe for Operation
Blanket Implementations§
source§impl<Q, K> Equivalent<K> for Qwhere
Q: Eq + ?Sized,
K: Borrow<Q> + ?Sized,
impl<Q, K> Equivalent<K> for Qwhere Q: Eq + ?Sized, K: Borrow<Q> + ?Sized,
source§fn equivalent(&self, key: &K) -> bool
fn equivalent(&self, key: &K) -> bool
Compare self to
key
and return true
if they are equal.