Frama-C:
Plug-ins:
Libraries:

Frama-C API - Eva_ast

Eva Syntax Tree.

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.Integer.t * ikind * string option
  3. | CString of Frama_c_kernel.Base.t
  4. | CChr of char
  5. | CReal of float * fkind * string option
  6. | 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

Structural comparaison 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.
val type_of_exp_node : Eva__.Eva_ast_types.exp_node -> Frama_c_kernel.Cil_types.typ
val type_of_lval_node : (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) -> Frama_c_kernel.Cil_types.typ
val type_of_lhost : Eva__.Eva_ast_types.lhost -> Frama_c_kernel.Cil_types.typ
val pp_lval : Stdlib.Format.formatter -> (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag -> unit
val pp_offset : Stdlib.Format.formatter -> Eva__.Eva_ast_types.offset -> unit
val pp_exp : Stdlib.Format.formatter -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag -> unit
val pp_constant : Stdlib.Format.formatter -> Eva__.Eva_ast_types.constant -> unit
val pp_unop : Stdlib.Format.formatter -> Eva__.Eva_ast_types.unop -> unit
val pp_binop : Stdlib.Format.formatter -> Eva__.Eva_ast_types.binop -> unit
module Lhost : Frama_c_kernel.Datatype.S_with_collections with type t = Eva__.Eva_ast_types.lhost
module Offset : Frama_c_kernel.Datatype.S_with_collections with type t = Eva__.Eva_ast_types.offset
module Lval : Frama_c_kernel.Datatype.S_with_collections with type t = (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag
module Exp : Frama_c_kernel.Datatype.S_with_collections with type t = Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag
module Constant : Frama_c_kernel.Datatype.S_with_collections with type t = Eva__.Eva_ast_types.constant
val mk_exp : Eva__.Eva_ast_types.exp_node -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag
val mk_lval : (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) -> (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag
val translate_exp : Frama_c_kernel.Cil_types.exp -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag
val translate_lval : Frama_c_kernel.Cil_types.lval -> (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag
val translate_offset : Frama_c_kernel.Cil_types.offset -> Eva__.Eva_ast_types.offset
val translate_unop : Frama_c_kernel.Cil_types.unop -> Eva__.Eva_ast_types.unop
val translate_binop : Frama_c_kernel.Cil_types.binop -> Eva__.Eva_ast_types.binop
val translate_init : Frama_c_kernel.Cil_types.init -> Eva__.Eva_ast_types.init
val invert_relation : Eva__.Eva_ast_types.binop -> Eva__.Eva_ast_types.binop

Inverse a relation, op must be a comparison operator

val conv_relation : Eva__.Eva_ast_types.binop -> Frama_c_kernel.Abstract_interp.Comp.t

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

val normalize_condition : Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag -> bool -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag

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.

val add_offset : (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag -> Eva__.Eva_ast_types.offset -> (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag
module Build : sig ... end

Conversion to Cil

val to_cil_exp : Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag -> Frama_c_kernel.Cil_types.exp
val to_cil_lval : (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag -> Frama_c_kernel.Cil_types.lval

Queries

val is_mutable : (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag -> bool

Cf Cil.is_mutable_or_initialized.

val is_initialized : (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag -> bool

Expressions/Lvalue heights

val height_exp : Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag -> int

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

val height_lval : (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag -> int

Computes the height of an lvalue.

Specialized visitors

val exp_contains_volatile : Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag -> 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__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag -> bool
val vars_in_exp : Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag -> Frama_c_kernel.Cil_datatype.Varinfo.Set.t

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

val vars_in_lval : (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag -> Frama_c_kernel.Cil_datatype.Varinfo.Set.t

Dependences of expressions and lvalues.

val zone_of_exp : ((Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag -> Frama_c_kernel.Precise_locs.precise_location) -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag -> Frama_c_kernel.Locations.Zone.t

Given a function computing the location of lvalues, computes the memory zone on which the value of an expression depends.

val zone_of_lval : ((Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag -> Frama_c_kernel.Precise_locs.precise_location) -> (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag -> Frama_c_kernel.Locations.Zone.t

Given a function computing the location of lvalues, computes the memory zone on which the value of an lvalue depends.

val indirect_zone_of_lval : ((Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag -> Frama_c_kernel.Precise_locs.precise_location) -> (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag -> Frama_c_kernel.Locations.Zone.t

Given a function computing the location of lvalues, computes the memory zone on which the offset and the pointer expression (if any) of an lvalue depend.

val deps_of_exp : ((Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag -> Frama_c_kernel.Precise_locs.precise_location) -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag -> Deps.t

Given a function computing the location of lvalues, computes the memory dependencies of an expression.

val deps_of_lval : ((Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag -> Frama_c_kernel.Precise_locs.precise_location) -> (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag -> Deps.t

Given a function computing the location of lvalues, computes the memory dependencies of an lvalue.

Constant conversion and folding.

val const_fold : Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag
val fold_to_integer : Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag -> Frama_c_kernel.Integer.t option
val is_zero_ptr : Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag -> bool

Offsets

val last_offset : Eva__.Eva_ast_types.offset -> Eva__.Eva_ast_types.offset

Returns the last offset in the chain.

val is_bitfield : (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag -> bool

Is an lvalue a bitfield?

module Rewrite : sig ... end

Folding visitor

module Fold : sig ... end