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
- Authors
-
- Maintainers
-
-
Michele Alberti
-
Thibaud Antignac
-
Gergö Barany
-
Patrick Baudin
-
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
-
Virgile Prevosto
-
Armand Puccetti
-
Virgile Robles
-
Muriel Roger
-
Julien Signoles
-
Kostyantyn Vorobyov
-
Boris Yakobowski
Sources
Dependencies
why3
>= "1.3.1" & < "1.4~"
conf-graphviz
post
lablgtk3
>= "3.0.beta4" & os != "macos"
lablgtk
>= "2.18.2"
conf-autoconf
build
ocamlgraph
>= "1.8.8" & < "1.9~"
ocaml
>= "4.05.0" & (< "4.08.0~" | >= "4.08.1")
Reverse Dependencies