Frama-C:
Plug-ins:
Libraries:

Frama-C API - Eva_ast

Eva Syntax Tree.

include module type of Eva_ast_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.
include module type of Eva_ast_typing
val type_of_exp_node : Eva_ast_types.exp_node -> Eva_ast_types.typ
val type_of_lval_node : Eva_ast_types.lval_node -> Eva_ast_types.typ
val type_of_lhost : Eva_ast_types.lhost -> Eva_ast_types.typ
include module type of Eva_ast_printer
val pp_lval : Stdlib.Format.formatter -> Eva_ast_types.lval -> unit
val pp_lhost : Stdlib.Format.formatter -> Eva_ast_types.lhost -> unit
val pp_offset : Stdlib.Format.formatter -> Eva_ast_types.offset -> unit
val pp_exp : Stdlib.Format.formatter -> Eva_ast_types.exp -> unit
val pp_constant : Stdlib.Format.formatter -> Eva_ast_types.constant -> unit
val pp_unop : Stdlib.Format.formatter -> Eva_ast_types.unop -> unit
val pp_binop : Stdlib.Format.formatter -> Eva_ast_types.binop -> unit
include module type of Eva_ast_datatype
include module type of Eva_ast_builder
val invert_relation : Eva_ast_types.binop -> Eva_ast_types.binop

Inverse a relation, op must be a comparison operator

Convert a relation to Abstract_interp.Comp, op must be a comparison operator

val normalize_condition : Eva_ast_types.exp -> bool -> Eva_ast_types.exp

normalize_condition e positive returns the expression corresponding to e != 0 when positive is true, and e == 0 otherwise. The resulting expression will always have a comparison operation at its root.

module Build : sig ... end
include module type of Eva_ast_deps
module type DepsOf = sig ... end

Dependencies of expressions and lvalues based on type location.

module type DepsOfInput = sig ... end

Input for MakeDepsOf functor.

Make DepsOf module based on a given location.

Dependencies of expressions and lvalues based on Precise_locs.precise_location.

include module type of Eva_ast_utils

Conversion to Cil

Queries

val is_mutable : Eva_ast_types.lval -> bool

Cf Cil.is_mutable_or_initialized.

val is_initialized : Eva_ast_types.lval -> bool

Expressions/Lvalue heights

val height_exp : Eva_ast_types.exp -> int

Computes the height of an expression, that is the maximum number of nested operations in this expression.

val height_lval : Eva_ast_types.lval -> int

Computes the height of an lvalue.

Specialized visitors

val exp_contains_volatile : Eva_ast_types.exp -> bool

exp_contains_volatile e (resp. lval_contains_volatile lv is true whenever one l-value contained inside the expression e (resp. the lvalue lv) has volatile qualifier. Relational analyses should not learn anything on such values.

val lval_contains_volatile : Eva_ast_types.lval -> bool

Returns the set of variables that syntactically appear in an expression or lvalue.

Constant conversion and folding.

val fold_to_integer : Eva_ast_types.exp -> Frama_c_kernel.Z.t option
val is_zero_ptr : Eva_ast_types.exp -> bool

Offsets

Returns the last offset in the chain.

val is_bitfield : Eva_ast_types.lval -> bool

Is an lvalue a bitfield?

include module type of Eva_ast_visitor
module Rewrite : sig ... end

Observing visitor

module Observe : sig ... end