Module gast

Definitions common to crate::ullbc_ast and crate::llbc_ast

Structs

• Assert
  Asserts are special constructs introduced by Rust to perform dynamic checks, to detect out-of-bounds accesses or divisions by zero for instance. We eliminate the assertions in [crate::remove_dynamic_checks], then introduce other dynamic checks in [crate::reconstruct_asserts].
• Call
• FunDecl
  A function definition
• FunDeclRef
  Reference to a function declaration.
• GExprBody
  An expression body. TODO: arg_count should be stored in GFunDecl below. But then, the print is obfuscated and Aeneas may need some refactoring.
• GlobalDecl
  A global variable definition (constant or static).
• GlobalDeclRef
  Reference to a global declaration.
• Locals
  The local variables of a body.
• Opaque
  Marker to indicate that a declaration is opaque (i.e. we don’t inspect its body).
• TraitDecl
  A trait declaration.
• TraitImpl
  A trait implementation.
• TraitItemName
• Var
  A variable

Enums

• AbortKind
• Body
  The body of a function or a constant.
• FnOperand
  A function operand is used in function calls. It either designates a top-level function, or a place in case we are using function pointers stored in local variables.
• ItemKind
  Item kind: whether this function/const is part of a trait declaration, trait implementation, or neither.