veri_ir

Module annotation_ir

Source

Structs§

BoundVar
A bound variable, including the VIR type
Const
Type-specified constants
TermAnnotation
Verification IR annotations for an ISLE term consist of the function signature and a list of assertions.
TermSignature
A function signature annotation, including the bound variable names for all arguments and the return value.

Enums§

Expr
Typed expressions (u32 is the type var)
Type
Higher-level type, not including bitwidths.
Width
Width arguments