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-Gallium.tar.gz
sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

doc/frama-c-wp.core/Wp/StmtSemantics/Make/index.html

Module StmtSemantics.MakeSource

Parameters

module _ : Memory.Compiler

Signature

Sourcetype node = Cfg.node
Sourcetype goal = {
  1. goal_pred : Cfg.P.t;
  2. goal_prop : WpPropId.prop_id;
}
Sourcetype cfg = Cfg.cfg
Sourcetype paths = {
  1. paths_cfg : cfg;
  2. paths_goals : goal Frama_c_kernel.Bag.t;
}
Sourceexception LabelNotFound of Clabels.c_label

Compilation environment

Sourcetype env
Sourceval bind : Clabels.c_label -> node -> env -> env
Sourceval result : env -> Lang.F.var
Sourceval (@^) : paths -> paths -> paths

Same as Cfg.concat

Sourceval (@*) : env -> (Clabels.c_label * node) list -> env

fold bind

Sourceval (@:) : env -> Clabels.c_label -> node

LabelMap.find with refined excpetion.

Sourceval (@-) : env -> (Clabels.c_label -> bool) -> env
Sourceval sequence : (env -> 'a -> paths) -> env -> 'a list -> paths

Chain compiler by introducing fresh nodes between each element of the list. For each consecutive x;y elements, a fresh node n is created, and x is compiled with Next:n and y is compiled with Here:n.

Sourceval choice : ?pre:Clabels.c_label -> ?post:Clabels.c_label -> (env -> 'a -> paths) -> env -> 'a list -> paths

Chain compiler in parallel, between labels ~pre and ~post, which defaults to resp. here and next. The list of eventualities is exhastive, hence an either assumption is also inserted.

Sourceval parallel : ?pre:Clabels.c_label -> ?post:Clabels.c_label -> (env -> 'a -> Cfg.C.t * paths) -> env -> 'a list -> paths

Chain compiler in parallel, between labels ~pre and ~post, which defaults to resp. here and next. The list of eventualities is exhastive, hence an either assumption is also inserted.

Instructions Compilation

Each instruction or statement is typically compiled between Here and Next nodes in the flow. Pre, Post and Exit are reserved for the entry and exit points of current function. in flow are used when needed such as Break and Continue and should be added before calling.

Sourceval return : env -> Frama_c_kernel.Cil_types.exp option -> paths
Sourceval assume : Cfg.P.t -> paths

ACSL Compilation

Sourceval assume_ : env -> Memory.polarity -> Frama_c_kernel.Cil_types.predicate -> paths

Automata Compilation

Sourceval init : is_pre_main:bool -> env -> paths

Full Compilation

Returns the set of all paths for the function, with all proof obligations. The returned node corresponds to the Init label.