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
copied = false, 2000)"
:class="{ 'border-gray-700': !copied, 'text-gray-100': !copied, 'focus:ring-orange-500': !copied, 'focus:border-orange-500': !copied, 'border-green-600': copied, 'text-green-600': copied, 'focus:ring-green-500': copied, 'focus:border-green-500': copied }">
- Published
- 07 Nov 2022
- Authors
-
-
Michele Alberti
-
Thibaud Antignac
-
Gergö Barany
-
Patrick Baudin
-
Thibaut Benjamin
-
Allan Blanchard
-
Lionel Blatter
-
François Bobot
-
Richard Bonichon
-
Quentin Bouillaguet
-
David Bühler
-
Zakaria Chihani
-
Loïc Correnson
-
Julien Crétin
-
Pascal Cuoq
-
Zaynah Dargaye
-
Basile Desloges
-
Jean-Christophe Filliâtre
-
Philippe Herrmann
-
Maxime Jacquemin
-
Florent Kirchner
-
Tristan Le Gall
-
Jean-Christophe Léchenet
-
Matthieu Lemerre
-
Dara Ly
-
David Maison
-
Claude Marché
-
André Maroneze
-
Thibault Martin
-
Fonenantsoa Maurica
-
Melody Méaulle
-
Benjamin Monate
-
Yannick Moy
-
Anne Pacalet
-
Valentin Perrelle
-
Guillaume Petiot
-
Dario Pinto
-
Virgile Prevosto
-
Armand Puccetti
-
Félix Ridoux
-
Virgile Robles
-
Muriel Roger
-
Julien Signoles
-
Kostyantyn Vorobyov
-
Boris Yakobowski
-
- 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"
zarith
>= "1.5"
yojson
>= "1.6.0" & (< "2.0.0" | !with-test)
why3
>= "1.5.1"
ocamlgraph
>= "1.8.8"
ocaml
>= "4.11.1"
conf-time
with-test
conf-graphviz
post
dune
(>= "3.2.0" & os != "macos") | (>= "3.5.0" & os = "macos")
Reverse Dependencies
Conflicts