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. A
    Anne Pacalet
  36. V
    Valentin Perrelle
  37. G
    Guillaume Petiot
  38. D
    Dario Pinto
  39. V
    Virgile Prevosto
  40. A
    Armand Puccetti
  41. F
    Félix Ridoux
  42. V
    Virgile Robles
  43. M
    Muriel Roger
  44. J
    Julien Signoles
  45. N
    Nicolas Stouls
  46. K
    Kostyantyn Vorobyov
  47. B
    Boris Yakobowski

Maintainers

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

Sources

frama-c-27.0-Cobalt.tar.gz
sha256=25885f89daa478aeafdd1e4205452c7a30695d4b3b3ee8fc98b4a9c5f83f79c2

doc/frama-c.kernel/Frama_c_kernel/Alarms/index.html

Module Frama_c_kernel.Alarms

Alarms Database.

type overflow_kind =
  1. | Signed
  2. | Unsigned
  3. | Signed_downcast
  4. | Unsigned_downcast
  5. | Pointer_downcast

Only signed overflows and pointer downcasts are really RTEs. The other kinds may be meaningful nevertheless.

type access_kind =
  1. | For_reading
  2. | For_writing
type bound_kind =
  1. | Lower_bound
  2. | Upper_bound
type alarm =
  1. | Division_by_zero of Cil_types.exp
  2. | Memory_access of Cil_types.lval * access_kind
  3. | Index_out_of_bound of Cil_types.exp * Cil_types.exp option
    (*

    Index_out_of_bound(index, opt)

    • opt = None -> lower bound is zero; Some up = upper bound
    *)
  4. | Invalid_pointer of Cil_types.exp
  5. | Invalid_shift of Cil_types.exp * int option
    (*

    strict upper bound, if any

    *)
  6. | Pointer_comparison of Cil_types.exp option * Cil_types.exp
    (*

    First parameter is None when implicit comparison to NULL pointer

    *)
  7. | Differing_blocks of Cil_types.exp * Cil_types.exp
    (*

    The two expressions (which evaluate to pointers) must point to the same allocated block

    *)
  8. | Overflow of overflow_kind * Cil_types.exp * Integer.t * bound_kind
    (*

    Integer parameters is the bound

    *)
  9. | Float_to_int of Cil_types.exp * Integer.t * bound_kind
    (*

    Integer parameter is the bound for the integer type. The actual alarm is exp < bound+1 or bound-1 < exp.

    *)
  10. | Not_separated of Cil_types.lval * Cil_types.lval
    (*

    the two lvalues must be separated

    *)
  11. | Overlap of Cil_types.lval * Cil_types.lval
    (*

    overlapping read/write: the two lvalues must be separated or equal

    *)
  12. | Uninitialized of Cil_types.lval
  13. | Dangling of Cil_types.lval
  14. | Is_nan_or_infinite of Cil_types.exp * Cil_types.fkind
  15. | Is_nan of Cil_types.exp * Cil_types.fkind
  16. | Function_pointer of Cil_types.exp * Cil_types.exp list option
    (*

    the type of the pointer is compatible with the type of the pointed function (first argument). The second argument is the list of the arguments of the call.

    *)
  17. | Invalid_bool of Cil_types.lval
    (*

    Trap representation of a _Bool variable.

    *)
include Datatype.S_with_collections with type t = alarm
include Datatype.S with type t = alarm
include Datatype.S_no_copy with type t = alarm
include Datatype.Ty with type t = alarm
type t = alarm
val ty : t Type.t
val name : string

Unique name of the datatype.

val descr : t Descr.t

Datatype descriptor.

val packed_descr : Structural_descr.pack

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 : (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.

module Set : Datatype.Set with type elt = t
module Map : Datatype.Map with type key = t
module Hashtbl : Datatype.Hashtbl with type key = t
val self : State.t

Register the given alarm on the given statement. By default, no status is emitted. kf must be given only if the kinstr is a statement, and must be the function enclosing this statement.

  • returns

    true if the given alarm has never been emitted before on the same kinstr (without taking into consideration the status or the emitter).

Conversion of an alarm to a code_annotation, without any registration. The returned boolean indicates that the alarm has not been registered in the kernel yet.

val iter : (Emitter.t -> Cil_types.kernel_function -> Cil_types.stmt -> rank:int -> alarm -> Cil_types.code_annotation -> unit) -> unit

Iterator over all alarms and the associated annotations at some program point.

  • since Fluorine-20130401
val fold : (Emitter.t -> Cil_types.kernel_function -> Cil_types.stmt -> rank:int -> alarm -> Cil_types.code_annotation -> 'a -> 'a) -> 'a -> 'a

Folder over all alarms and the associated annotations at some program point.

  • since Fluorine-20130401

Returns the sequence of all alarms and the associated annotations at some program point

  • since 26.0-Iron
val find : Cil_types.code_annotation -> alarm option
  • returns

    the alarm corresponding to the given assertion, if any.

  • since Fluorine-20130401
val remove : ?filter:(alarm -> bool) -> ?kinstr:Cil_types.kinstr -> Emitter.t -> unit

Remove the alarms and the associated annotations emitted by the given emitter. If kinstr is specified, remove only the ones associated with this kinstr. If filter is specified, remove only the alarms a such that filter a is true.

  • since Fluorine-20130401
val create_predicate : ?loc:Cil_types.location -> t -> Cil_types.predicate

Generate the predicate corresponding to a given alarm.

  • since Fluorine-20130401
val get_name : t -> string

Short name of the alarm, used to prefix the assertion in the AST.

val get_short_name : t -> string

Even shorter name. Similar alarms (e.g. signed overflow vs. unsigned overflow) are aggregated.

val get_description : t -> string

Long description of the alarm, explaining the UB it guards against.