package frama-c

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

Install

frama-c.com Readme LGPL-2.1-only License Edit opam file

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. T
    Tristan Le Gall
  23. J
    Jean-Christophe Léchenet
  24. M
    Matthieu Lemerre
  25. D
    Dara Ly
  26. D
    David Maison
  27. C
    Claude Marché
  28. A
    André Maroneze
  29. T
    Thibault Martin
  30. F
    Fonenantsoa Maurica
  31. M
    Melody Méaulle
  32. B
    Benjamin Monate
  33. Y
    Yannick Moy
  34. A
    Anne Pacalet
  35. V
    Valentin Perrelle
  36. G
    Guillaume Petiot
  37. D
    Dario Pinto
  38. V
    Virgile Prevosto
  39. A
    Armand Puccetti
  40. F
    Félix Ridoux
  41. V
    Virgile Robles
  42. M
    Muriel Roger
  43. J
    Julien Signoles
  44. K
    Kostyantyn Vorobyov
  45. B
    Boris Yakobowski

Maintainers

  1. F
    francois.bobot@cea.fr

Sources

frama-c-26.0-beta-Iron.tar.gz
sha256=d4cce05ab46d66a10664fc3432181b9cbb2edc32a759ce280541c719135ca7e7

Description

Frama-C gathers several analysis techniques in a single collaborative framework, based on analyzers (called "plug-ins") that can build upon the results computed by other analyzers in the framework. Thanks to this approach, Frama-C provides sophisticated tools, including:

  • an analyzer based on abstract interpretation (Eva plug-in);
  • a program proof framework based on weakest precondition calculus (WP plug-in);
  • a program slicer (Slicing plug-in);
  • a tool for verification of temporal (LTL) properties (Aoraï plug-in);
  • a runtime verification tool (E-ACSL plug-in);
  • several tools for code base exploration and dependency analysis (plug-ins From, Impact, Metrics, Occurrence, Scope, etc.). These plug-ins communicate between each other via the Frama-C API and via ACSL (ANSI/ISO C Specification Language) properties.

Tags

deductive program verification formal specification automated theorem prover interactive theorem prover C plugins abstract interpretation slicing weakest precondition ACSL dataflow analysis runtime verification

Published: 07 Nov 2022

Dependencies (23)

  1. conf-gtksourceview3 os != "macos"
  2. lablgtk3-sourceview3 os != "macos"
  3. lablgtk3 >= "3.1.0" & os != "macos"
  4. ocamlgraph_gtk os = "macos"
  5. ocamlgraph < "2.0" & os = "macos"
  6. conf-gtksourceview os = "macos"
  7. conf-gnomecanvas os = "macos"
  8. lablgtk >= "2.18.8" & os = "macos"
  9. ppx_import
  10. ppx_deriving_yojson
  11. ppx_deriving
  12. zarith >= "1.5"
  13. why3 >= "1.5.1" & < "1.6~"
  14. ocamlgraph >= "1.8.8"
  15. ocamlfind
  16. ocaml >= "4.11.1"
  17. conf-graphviz post
  18. alt-ergo
  19. alt-ergo-free
  20. dune-site >= "3.2.0"
  21. dune-private-libs
  22. dune-configurator
  23. dune (>= "3.2.0" & os != "macos") | (>= "3.5.0" & os = "macos")

Dev Dependencies (3)

  1. yojson >= "1.6.0" & < "2.1.0" & (< "2.0.0" | !with-test)
  2. ocamlgraph with-test & < "2.1.0"
  3. conf-time with-test

Used by (3)

  1. frama-c-metacsl = "0.4"
  2. pilat < "1.2" | >= "1.6"
  3. why < "2.32"

Conflicts (4)

  1. result < "1.5"
  2. pilat <= "1.6"
  3. mlmpfr < "4.1.0-bugfix2"
  4. cairo2 < "0.6.2"