package frama-c

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

Install 

dune-project
 Dependency

frama-c.com Edit opam file Versions (30)

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. N
    Nicolas Stouls
  45. K
    Kostyantyn Vorobyov
  46. B
    Boris Yakobowski

Maintainers

  1. F
    francois.bobot@cea.fr

Sources

frama-c-26.0-Iron.tar.gz
sha256=5b51102dd44309d7b8b44dd10221716c9915e0ebb0e65817a50b32ee6e79afd9

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

Added to opam-repository:

Dependencies (18)

  1. conf-gtksourceview3 os != "macos"
  2. lablgtk3-sourceview3 os != "macos"
  3. lablgtk3 >= "3.1.0" & os != "macos"
  4. ppx_import
  5. ppx_deriving_yojson
  6. ppx_deriving
  7. zarith >= "1.5"
  8. why3 >= "1.5.1" & < "1.6~"
  9. ocamlgraph >= "1.8.8"
  10. ocamlfind
  11. ocaml >= "4.11.1" & < "5.3"
  12. conf-graphviz post
  13. alt-ergo
  14. alt-ergo-free
  15. dune-site >= "3.2.0"
  16. dune-private-libs
  17. dune-configurator
  18. 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

Optional Dependencies (3)

  1. zmq
  2. mlmpfr
  3. apron

Used by (2)

  1. frama-c-metacsl = "0.4"
  2. pilat != "1.2"

Conflicts (4)

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

Build status

Results of building frama-c with each compiler on check.ci.ocaml.org, run of against opam-repository 7cdc698. All results for this package.

Each result links to its build log. To keep crawlers from overloading the site, build logs require a GitHub sign-in (see ocurrent/opam-health-check). On your first log, GitHub asks you to “Authorize opam-health-check”, the OCurrent app that runs these checks; it sees only your public profile, not your repositories. The sign-in lasts 30 days.

This version is not in the latest run; the versions below are.

Version OCaml 4.11 OCaml 4.14 OCaml 5.2 OCaml 5.4 OCaml 5.5
33.0 n/a good good good good
27.1 good good good n/a n/a
  • good Package successfully built
  • partial One of the dependencies failed to build
  • bad Package failed to build
  • n/a Package is not available in this environment
  • internal Internal failure