Frama-C:
Plug-ins:
Libraries:

Frama-C API - Eva_ast_types

Types definition of the Eva AST for lvalues and expressions. Should also include ACSL terms and predicates in the future. Most types are similar to Cil_types.

type 'a tag = private {
  1. node : 'a;
  2. typ : Frama_c_kernel.Cil_types.typ;
  3. origin : origin;
}
type exp = exp_node tag
and exp_node =
  1. | Const of constant
  2. | Lval of lval
  3. | UnOp of unop * exp * typ
  4. | BinOp of binop * exp * exp * typ
  5. | CastE of typ * exp
  6. | AddrOf of lval
  7. | StartOf of lval
and constant =
  1. | CTopInt of ikind
  2. | CInt64 of Frama_c_kernel.Z.t * ikind * string option
  3. | CChr of char
  4. | CReal of float * fkind * string option
  5. | CEnum of Frama_c_kernel.Cil_types.enumitem * exp

Constants

and lval = lval_node tag
and lval_node = lhost * offset
and lhost =
  1. | Var of varinfo
  2. | Mem of exp
and offset =
  1. | NoOffset
  2. | Field of Frama_c_kernel.Cil_types.fieldinfo * offset
  3. | Index of exp * offset
and unop =
  1. | Neg
  2. | BNot
  3. | LNot
and binop =
  1. | PlusA
  2. | PlusPI
  3. | MinusA
  4. | MinusPI
  5. | MinusPP
  6. | Mult
  7. | Div
  8. | Mod
  9. | Shiftlt
  10. | Shiftrt
  11. | Lt
  12. | Gt
  13. | Le
  14. | Ge
  15. | Eq
  16. | Ne
  17. | BAnd
  18. | BXor
  19. | BOr
  20. | LAnd
  21. | LOr
type init =
  1. | SingleInit of exp * Frama_c_kernel.Cil_types.location
  2. | CompoundInit of typ * (offset * init) list
type init_or_str =
  1. | CInit of init
  2. | StrInit of Frama_c_kernel.Cil_types.str_literal

Structural comparison and equality functions, generated by ppx deriving. Equivalent to the functions provided by Cil_datatype.ConstantStrict and Cil_datatype.ExpStructEqStrict.

val compare_constant : constant -> constant -> int
val equal_constant : constant -> constant -> bool
val compare_exp : exp -> exp -> int
val equal_exp : exp -> exp -> bool
val compare_lval : lval -> lval -> int
val equal_lval : lval -> lval -> bool
val compare_lhost : lhost -> lhost -> int
val equal_lhost : lhost -> lhost -> bool
val compare_offset : offset -> offset -> int
val equal_offset : offset -> offset -> bool
val mk_tag : node:'a -> typ:Frama_c_kernel.Cil_types.typ -> origin:origin -> 'a tag

Tag builder for Eva_ast_builder only. 

  • alert eva_ast_builder For internal use only; use mk_exp and mk_lval builders instead.