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. T
    Thibaut Benjamin
  6. A
    Allan Blanchard
  7. L
    Lionel Blatter
  8. F
    François Bobot
  9. R
    Richard Bonichon
  10. Q
    Quentin Bouillaguet
  11. D
    David Bühler
  12. Z
    Zakaria Chihani
  13. L
    Loïc Correnson
  14. J
    Julien Crétin
  15. P
    Pascal Cuoq
  16. Z
    Zaynah Dargaye
  17. B
    Basile Desloges
  18. J
    Jean-Christophe Filliâtre
  19. P
    Philippe Herrmann
  20. M
    Maxime Jacquemin
  21. F
    Florent Kirchner
  22. A
    Alexander Kogtenkov
  23. T
    Tristan Le Gall
  24. J
    Jean-Christophe Léchenet
  25. M
    Matthieu Lemerre
  26. D
    Dara Ly
  27. D
    David Maison
  28. C
    Claude Marché
  29. A
    André Maroneze
  30. T
    Thibault Martin
  31. F
    Fonenantsoa Maurica
  32. M
    Melody Méaulle
  33. B
    Benjamin Monate
  34. Y
    Yannick Moy
  35. P
    Pierre Nigron
  36. A
    Anne Pacalet
  37. V
    Valentin Perrelle
  38. G
    Guillaume Petiot
  39. D
    Dario Pinto
  40. V
    Virgile Prevosto
  41. A
    Armand Puccetti
  42. F
    Félix Ridoux
  43. V
    Virgile Robles
  44. J
    Jan Rochel
  45. M
    Muriel Roger
  46. J
    Julien Signoles
  47. N
    Nicolas Stouls
  48. K
    Kostyantyn Vorobyov
  49. B
    Boris Yakobowski

Maintainers

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

Sources

frama-c-28.0-Nickel.tar.gz
sha256=29612882330ecb6eddd0b4ca3afc0492b70d0feb3379a1b8e893194c6e173983

doc/frama-c-eva.gui/Eva_gui/Gui_eval/Make/argument-1-X/Val/index.html

Module X.Val

include Frama_c_kernel.Datatype.S
include Frama_c_kernel.Datatype.S_no_copy
include Frama_c_kernel.Datatype.Ty
type t
val name : string

Unique name of the datatype.

Datatype descriptor.

Packed version of the descriptor.

val reprs : t list

List of representants of the descriptor.

val equal : t -> t -> bool

Equality: same spec than Stdlib.(=).

val compare : t -> t -> int

Comparison: same spec than Stdlib.compare.

val hash : t -> int

Hash function: same spec than Hashtbl.hash.

val pretty : Format.formatter -> t -> unit

Pretty print each value in an user-friendly way.

val mem_project : (Frama_c_kernel.Project_skeleton.t -> bool) -> t -> bool

mem_project f x must return true iff there is a value p of type Project.t in x such that f p returns true.

val copy : t -> t

Deep copy: no possible sharing between x and copy x.

Pretty the abstract value assuming it has the type given as argument.

Lattice Structure

val top : t
val is_included : t -> t -> bool
val join : t -> t -> t
val narrow : t -> t -> t Eva.Eval.or_bottom

Constructors

val zero : t
val one : t
val top_int : t

Abstract address for the given varinfo. (With type "pointer to the type of the variable" if the abstract values are typed.)

Alarms

These functions are used to create the alarms that report undesirable behaviors, when a value abstraction does not meet the prerequisites of an operation. Thereafter, the value is assumed to meet them to continue the analysis. See the documentation of the truth type for more details.

val assume_non_zero : t -> [ `False | `Unknown of t | `True | `TrueReduced of t | `Unreachable ]
val assume_bounded : Frama_c_kernel.Alarms.bound_kind -> Eva__.Abstract_value.bound -> t -> [ `False | `Unknown of t | `True | `TrueReduced of t | `Unreachable ]
val assume_not_nan : assume_finite:bool -> Frama_c_kernel.Cil_types.fkind -> t -> [ `False | `Unknown of t | `True | `TrueReduced of t | `Unreachable ]
val assume_pointer : t -> [ `False | `Unknown of t | `True | `TrueReduced of t | `Unreachable ]

Assumes that the abstract value only represents well-formed pointer values: pointers either to an element of an array object or one past the last element of an array object. (A pointer to an object that is not an element of an array is viewed as a pointer to the first element of an array of length one with the type of the object as its element type.) The NULL pointer is always a valid pointer value. Function pointers are also considered as valid pointer values for now.

val assume_comparable : Eva__.Abstract_value.pointer_comparison -> t -> t -> [ `False | `Unknown of t * t | `True | `TrueReduced of t * t | `Unreachable ]

Forward Operations

Embeds C constants into value abstractions: returns an abstract value for the given constant. The constant cannot be an enumeration constant.

forward_unop typ unop v evaluates the value unop v, resulting from the application of the unary operator unop to the value v. typ is the type of v.

forward_binop typ binop v1 v2 evaluates the value v1 binop v2, resulting from the application of the binary operator binop to the values v1 and v2. typ is the type of v1.

val rewrap_integer : Eva__.Eval_typ.integer_range -> t -> t

rewrap_integer irange t wraps around the abstract value t to fit the integer range irange, assuming 2's complement.

val forward_cast : src_type:Eva__.Eval_typ.scalar_typ -> dst_type:Eva__.Eval_typ.scalar_typ -> t -> t Eva.Eval.or_bottom

Abstract evaluation of casts operators from src_type to dst_type.

Backward Operations

For an unary forward operation F, the inverse backward operator B tries to reduce the argument values of the operation, given its result.

It must satisfy: if B arg res = v then ∀ a ⊆ arg such that F a ⊆ res, a ⊆ v

i.e. B arg res returns a value v larger than all subvalues of arg whose result through F is included in res.

If F arg ∈ res is impossible, then v should be bottom. If the value arg cannot be reduced, then v should be None.

Any n-ary operator may be considered as a unary operator on a vector of values, the inclusion being lifted pointwise.

val backward_binop : input_type:Frama_c_kernel.Cil_types.typ -> resulting_type:Frama_c_kernel.Cil_types.typ -> Frama_c_kernel.Cil_types.binop -> left:t -> right:t -> result:t -> (t option * t option) Eva.Eval.or_bottom

Backward evaluation of the binary operation left binop right = result; tries to reduce the argument left and right according to result. input_type is the type of left, resulting_type the type of result.

val backward_unop : typ_arg:Frama_c_kernel.Cil_types.typ -> Frama_c_kernel.Cil_types.unop -> arg:t -> res:t -> t option Eva.Eval.or_bottom

Backward evaluation of the unary operation unop arg = res; tries to reduce the argument arg according to res. typ_arg is the type of arg.

val backward_cast : src_typ:Frama_c_kernel.Cil_types.typ -> dst_typ:Frama_c_kernel.Cil_types.typ -> src_val:t -> dst_val:t -> t option Eva.Eval.or_bottom

Backward evaluation of the cast of the value src_val of type src_typ into the value dst_val of type dst_typ. Tries to reduce scr_val according to dst_val.

Misc

val resolve_functions : t -> Frama_c_kernel.Kernel_function.t list Eva.Eval.or_top * bool

resolve_functions v returns the list of functions that may be pointed to by the abstract value v (representing a function pointer). The returned boolean must be true if some of the values represented by v do not correspond to functions. It is always safe to return `Top, true.

val replace_base : Frama_c_kernel.Base.substitution -> t -> t

For pointer values, replace_base substitution value replaces the bases pointed to by value according to substitution. For arithmetic values, this function returns the value unchanged.

val structure : t Eva__.Abstract.Value.structure
val mem : 'a Eva__.Structure.Key_Value.key -> bool

Tests whether a key belongs to the module.

val get : 'a Eva__.Structure.Key_Value.key -> (t -> 'a) option

For a key of type k key:

  • if the values of type t contain a subpart of type k from a module identified by the key, then get key returns an accessor for it.
  • otherwise, get key returns None.
val set : 'a Eva__.Structure.Key_Value.key -> 'a -> t -> t

For a key of type k key:

  • if the values of type t contain a subpart of type k from a module identified by the key, then set key v t returns the value t in which this subpart has been replaced by v.
  • otherwise, set key _ is the identity function.

Iterators on the components of a structure.

type polymorphic_iter_fun = {
  1. iter : 'a. 'a Eva__.Structure.Key_Value.key -> (module Eva__.Abstract_value.S with type t = 'a) -> 'a -> unit;
}
val iter : polymorphic_iter_fun -> t -> unit
type 'b polymorphic_fold_fun = {
  1. fold : 'a. 'a Eva__.Structure.Key_Value.key -> (module Eva__.Abstract_value.S with type t = 'a) -> 'a -> 'b -> 'b;
}
val fold : 'b polymorphic_fold_fun -> t -> 'b -> 'b
type polymorphic_map_fun = {
  1. map : 'a. 'a Eva__.Structure.Key_Value.key -> (module Eva__.Abstract_value.S with type t = 'a) -> 'a -> 'a;
}
val map : polymorphic_map_fun -> t -> t
val reduce : t -> t