package frama-c

  1. Overview
  2. Docs
Platform dedicated to the analysis of source code written in C

Install 

dune-project
 Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

  1. M
    Michele Alberti
  2. T
    Thibaud Antignac
  3. G
    Gergö Barany
  4. P
    Patrick Baudin
  5. N
    Nicolas Bellec
  6. T
    Thibaut Benjamin
  7. A
    Allan Blanchard
  8. L
    Lionel Blatter
  9. F
    François Bobot
  10. R
    Richard Bonichon
  11. V
    Vincent Botbol
  12. Q
    Quentin Bouillaguet
  13. D
    David Bühler
  14. Z
    Zakaria Chihani
  15. S
    Sylvain Chiron
  16. L
    Loïc Correnson
  17. J
    Julien Crétin
  18. P
    Pascal Cuoq
  19. Z
    Zaynah Dargaye
  20. B
    Basile Desloges
  21. J
    Jean-Christophe Filliâtre
  22. P
    Philippe Herrmann
  23. M
    Maxime Jacquemin
  24. B
    Benjamin Jorge
  25. F
    Florent Kirchner
  26. A
    Alexander Kogtenkov
  27. R
    Remi Lazarini
  28. T
    Tristan Le Gall
  29. K
    Kilyan Le Gallic
  30. J
    Jean-Christophe Léchenet
  31. M
    Matthieu Lemerre
  32. D
    Dara Ly
  33. D
    David Maison
  34. C
    Claude Marché
  35. A
    André Maroneze
  36. T
    Thibault Martin
  37. F
    Fonenantsoa Maurica
  38. M
    Melody Méaulle
  39. B
    Benjamin Monate
  40. Y
    Yannick Moy
  41. P
    Pierre Nigron
  42. A
    Anne Pacalet
  43. V
    Valentin Perrelle
  44. G
    Guillaume Petiot
  45. D
    Dario Pinto
  46. V
    Virgile Prevosto
  47. A
    Armand Puccetti
  48. F
    Félix Ridoux
  49. V
    Virgile Robles
  50. J
    Jan Rochel
  51. M
    Muriel Roger
  52. C
    Cécile Ruet-Cros
  53. J
    Julien Signoles
  54. N
    Nicolas Stouls
  55. K
    Kostyantyn Vorobyov
  56. B
    Boris Yakobowski

Maintainers

  1. F
    frama-ci-bot@frama-c.com

Sources

frama-c-31.0-beta-Gallium.tar.gz
sha256=095ffbb3086a6cd963a03e3defab4f0dc32e9a43f026e552ec9ae346a6e20522

doc/frama-c-eva.core/Eva/Eva_ast/index.html

Module Eva.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 : 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
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.

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

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