package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 : Format.formatter -> (Eva__.Eva_ast_types.lhost * Eva__.Eva_ast_types.offset) Eva__.Eva_ast_types.tag -> unit
val pp_offset : Format.formatter -> Eva__.Eva_ast_types.offset -> unit
val pp_exp : Format.formatter -> Eva__.Eva_ast_types.exp_node Eva__.Eva_ast_types.tag -> unit
val pp_constant : Format.formatter -> Eva__.Eva_ast_types.constant -> unit
val pp_unop : Format.formatter -> Eva__.Eva_ast_types.unop -> unit
val pp_binop : 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct