Module bytecode::stackless_bytecode

source ·

Structs

  • AbortAction
    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.
  • AttrId
    An id for an attribute attached to an instruction.
  • BorrowEdgeDisplay
  • BorrowNodeDisplay
    A display object for a borrow node.
  • BytecodeDisplay
    A display object for a bytecode.
  • Label
    A label for a branch destination.
  • OperationDisplay
    A display object for an operation.
  • SpecBlockId
    An id for a spec block. A spec block can contain assumes and asserts to be enforced at a program point.

Enums

  • AssignKind
    The kind of an assignment in the bytecode.
  • BorrowEdge
    A borrow edge.
  • BorrowNode
    A borrow node – used in memory operations.
  • Bytecode
    The stackless bytecode.
  • Constant
    A constant value.
  • HavocKind
    The type of variable that is being havoc-ed
  • Operation
    An operation – target of a call. This contains user functions, builtin functions, and operators.
  • PropKind
    A specification property kind.