Structs
Information about the action to take on abort. The label represents the destination to jump to, and the temporary where to store the abort code before jump.
An id for an attribute attached to an instruction.
A display object for a borrow node.
A display object for a bytecode.
A label for a branch destination.
A display object for an operation.
An id for a spec block. A spec block can contain assumes and asserts to be enforced at a program point.
Enums
The kind of an assignment in the bytecode.
A borrow edge.
A borrow node – used in memory operations.
The stackless bytecode.
A constant value.
The type of variable that is being havoc-ed
An operation – target of a call. This contains user functions, builtin functions, and operators.
A specification property kind.