package frama-c

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

Install

frama-c.com 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. 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-beta-Cobalt.tar.gz
sha256=9c1b14a689ac8ccda9e827c2eede13bb8d781fb8e4e33c1b5360408e312127d2

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: 17 May 2023

Dependencies (20)

  1. conf-gtksourceview3 os != "macos"
  2. lablgtk3-sourceview3 os != "macos"
  3. lablgtk3 >= "3.1.0" & os != "macos"
  4. ppx_import
  5. ppx_deriving_yaml >= "0.2.0"
  6. ppx_deriving_yojson
  7. ppx_deriving
  8. zarith >= "1.5"
  9. yaml >= "3.0.0"
  10. why3 >= "1.6.0"
  11. ocamlgraph >= "1.8.8"
  12. ocamlfind
  13. ocaml >= "4.11.1"
  14. menhir >= "20181006" & build
  15. conf-graphviz post
  16. alt-ergo
  17. alt-ergo-free
  18. dune-site
  19. dune-configurator
  20. dune >= "3.2.0" | (>= "3.5.0" & os = "macos")

Dev Dependencies (3)

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

Used by (4)

  1. frama-c-metacsl >= "0.5~beta"
  2. frama-clang
  3. pilat < "1.2" | >= "1.6"
  4. why < "2.32"

Conflicts (4)

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