Expand description
Definitions common to crate::ullbc_ast and crate::llbc_ast
Macros§
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
- Copy
NonOverlapping - DeclRef
- A generic
*DeclRef-shaped struct, used when we’re generic over the type of item. - 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
Assoc Const - An associated constant in a trait.
- Trait
Assoc Ty - An associated type in a trait.
- Trait
Assoc TyImpl - The value of a trait associated type.
- Trait
Decl - A trait declaration.
- Trait
Impl - A trait implementation.
- Trait
Item Name - Trait
Method - A trait method.
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
Source - Item kind: whether this function/const is part of a trait declaration, trait implementation, or neither.