frama-c

Platform dedicated to the analysis of source code written in C
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.
Install
deductive program verification formal specification automated theorem prover interactive theorem prover C plugins abstract interpretation slicing weakest precondition ACSL dataflow analysis runtime verification
Documentation frama-c.com LGPL-2.1-only License Edit opam file
Published
07 Nov 2022
Authors
Maintainers
Sources
frama-c-26.0-beta-Iron.tar.gz
sha256=d4cce05ab46d66a10664fc3432181b9cbb2edc32a759ce280541c719135ca7e7
Dependencies
conf-gtksourceview3 os != "macos"
lablgtk3-sourceview3 os != "macos"
lablgtk3 >= "3.1.0" & os != "macos"
ocamlgraph_gtk os = "macos"
ocamlgraph < "2.0" & os = "macos"
conf-gtksourceview os = "macos"
conf-gnomecanvas os = "macos"
lablgtk >= "2.18.8" & os = "macos"
ppx_import
ppx_deriving_yojson
ppx_deriving
zarith >= "1.5"
yojson >= "1.6.0" & (< "2.0.0" | !with-test)
why3 >= "1.5.1"
ocamlgraph >= "1.8.8"
ocamlfind
ocaml >= "4.11.1"
conf-time with-test
conf-graphviz post
alt-ergo
alt-ergo-free
dune-site
dune-private-libs
dune-configurator
dune (>= "3.2.0" & os != "macos") | (>= "3.5.0" & os = "macos")
Reverse Dependencies
frama-c-metacsl >= "0.4"
pilat < "1.2" | >= "1.6"
why < "2.32"
Conflicts
result < "1.5"
pilat <= "1.6"
mlmpfr < "4.1.0-bugfix2"
cairo2 < "0.6.2"