Expand description
Definitions common to crate::ullbc_ast and crate::llbc_ast
Structs§
- Assert
- Check the value of an operand and abort if the value is not expected. This is introduced to avoid a lot of small branches.
- Call
- FunDecl
- A function definition
- FunDecl
Ref - Reference to a function declaration.
- GExpr
Body - An expression body. TODO: arg_count should be stored in GFunDecl below. But then, the print is obfuscated and Aeneas may need some refactoring.
- Global
Decl - A global variable definition (constant or static).
- Global
Decl Ref - Reference to a global declaration.
- Local
- A variable
- Locals
- The local variables of a body.
- Opaque
- Marker to indicate that a declaration is opaque (i.e. we don’t inspect its body).
- Trait
Decl - A trait declaration.
- Trait
Impl - A trait implementation.
- Trait
Item Name
Enums§
- Abort
Kind - (U)LLBC is a language with side-effects: a statement may abort in a way that isn’t tracked by control-flow. The two kinds of abort are:
- 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.
- Global
Kind - Item
Kind - Item kind: whether this function/const is part of a trait declaration, trait implementation, or neither.