Module gast

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

Re-exports

• pub use super::gast_utils::*;

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].
• BodyId
• Call
• FunDecl
  A function definition
• FunDeclId
• 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
• GlobalDeclRef
  Reference to a global declaration.
• 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.