package frama-c

  1. Overview
  2. Docs

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.

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"