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

Maintainers

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

Sources

frama-c-29.0-Copper.tar.gz
sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c-wp.core/Wp/StmtSemantics/Make/argument-1-Compiler/C/index.html

Module Compiler.C

module M = M

The underlying memory model

type loc = M.loc
type nonrec value = loc Sigs.value
type nonrec result = loc Sigs.result
type sigma = M.Sigma.t
val pp_value : Format.formatter -> value -> unit
val cval : value -> Lang.F.term

Evaluate an abstract value. May fail because of M.pointer_val.

val cloc : value -> loc

Interpret a value as a location. May fail because of M.pointer_loc.

Applies a pointer cast or a conversion.

cast tr te ve transforms a value ve with type te into a value with type tr.

Computes the value of (a==b) provided both a and b are values with the given type.

Computes the value of (a==b) provided both a and b are values with the given type.

val equal_obj : Ctypes.c_object -> value -> value -> Lang.F.pred

Same as equal_typ with an object type.

val not_equal_obj : Ctypes.c_object -> value -> value -> Lang.F.pred

Same as not_equal_typ with an object type.

Evaluate the expression on the given memory state.

Evaluate the conditional expression on the given memory state.

Evaluate the left-value on the given memory state.

Address of a function pointer. Handles AddrOf, StartOf and Lval as usual.

Check whether a function pointer is (an instance of) some kernel function. Currently, the meaning of "being an instance of" is simply equality.

val loc_of_exp : sigma -> Frama_c_kernel.Cil_types.exp -> loc

Compile an expression as a location. May (also) fail because of M.pointer_val.

Compile an expression as a term. May (also) fail because of M.pointer_loc.

Value of an abstract result container.

Return an expression with a given type. Short cut for compiling the expression, cast into the desired type, and finally converted to a term.

val is_zero : sigma -> Ctypes.c_object -> loc -> Lang.F.pred

Express that the object (of specified type) at the given location is filled with zeroes.

val is_exp_range : sigma -> loc -> Ctypes.c_object -> Lang.F.term -> Lang.F.term -> value option -> Lang.F.pred

Express that all objects in a range of locations have a given value.

More precisely, is_exp_range sigma loc ty a b v express that value at ( ty* )loc + k equals v, forall a <= k <= b. Value v=None stands for zero.

Express that a given variable has the same value in two memory states.

type warned_hyp = Warning.Set.t * (Lang.F.pred * Lang.F.pred)

Express that some variable has some initial value at the given memory state. The first predicate states the value, the second, the initialization status.

Note: we DO NOT merge values and initialization status hypotheses as the factorization performed by Qed can make predicates too hard to simplify later.

Remark: None initializer are interpreted as zeroes. This is consistent with the init option associated with global variables in CIL, for which the default initializer are zeroes. This function is called for global initializers and local initializers (Cil.Local_init). It is not called for local variables without initializers as they do not have a Cil.init option.