package frama-c
Install
Dune Dependency
Authors
-
MMichele Alberti
-
TThibaud Antignac
-
GGergö Barany
-
PPatrick Baudin
-
NNicolas Bellec
-
TThibaut Benjamin
-
AAllan Blanchard
-
LLionel Blatter
-
FFrançois Bobot
-
RRichard Bonichon
-
VVincent Botbol
-
QQuentin Bouillaguet
-
DDavid Bühler
-
ZZakaria Chihani
-
LLoïc Correnson
-
JJulien Crétin
-
PPascal Cuoq
-
ZZaynah Dargaye
-
BBasile Desloges
-
JJean-Christophe Filliâtre
-
PPhilippe Herrmann
-
MMaxime Jacquemin
-
FFlorent Kirchner
-
AAlexander Kogtenkov
-
RRemi Lazarini
-
TTristan Le Gall
-
JJean-Christophe Léchenet
-
MMatthieu Lemerre
-
DDara Ly
-
DDavid Maison
-
CClaude Marché
-
AAndré Maroneze
-
TThibault Martin
-
FFonenantsoa Maurica
-
MMelody Méaulle
-
BBenjamin Monate
-
YYannick Moy
-
PPierre Nigron
-
AAnne Pacalet
-
VValentin Perrelle
-
GGuillaume Petiot
-
DDario Pinto
-
VVirgile Prevosto
-
AArmand Puccetti
-
FFélix Ridoux
-
VVirgile Robles
-
JJan Rochel
-
MMuriel Roger
-
JJulien Signoles
-
NNicolas Stouls
-
KKostyantyn Vorobyov
-
BBoris Yakobowski
Maintainers
Sources
sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493
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 verificationPublished: 13 Jun 2024
README
README.md
Frama-C is a platform dedicated to the analysis of source code written in C.
A Collaborative Platform
Frama-C gathers several analysis techniques in a single collaborative platform, consisting of a kernel providing a core set of features (e.g., a normalized AST for C programs) plus a set of analyzers, called plug-ins. Plug-ins can build upon results computed by other plug-ins in the platform.
Thanks to this approach, Frama-C provides sophisticated tools, including:
an analyzer based on abstract interpretation, aimed at verifying the absence of run-time errors (Eva);
a program proof framework based on weakest precondition calculus (WP);
a program slicer (Slicing);
a tool for verification of temporal (LTL) properties (Aoraï);
a runtime verification tool (E-ACSL);
several tools for code base exploration and dependency analysis (From, Impact, Metrics, Occurrence, Scope, etc.).
These plug-ins share a common language and can exchange information via ACSL (ANSI/ISO C Specification Language) properties. Plug-ins can also collaborate via their APIs.
Installation
Frama-C is available through opam, the OCaml package manager. If you have it, simply run:
opam install frama-c
or, for opam
versions less than 2.1:
opam install depext # handles external (non-OCaml) dependencies
opam depext frama-c --install
Frama-C is developed mainly in Linux, often tested in macOS (via Homebrew), and occasionally tested on Windows (via the Windows Subsystem for Linux).
For detailed installation instructions and troubleshooting, see INSTALL.md.
Development branch
To install the development branch of Frama-C (updated nightly):
opam pin add frama-c --dev-repo
This command will pin the development version of Frama-C and try to install it. If installation fails due to missing external dependencies, try using the same commands from the Installation section to get the external dependencies and then install Frama-C.
Distribution packages
Some Linux distributions have a frama-c
package, kindly provided by distribution packagers. Note that they may not correspond to the latest Frama-C release.
Usage
Frama-C can be run from the command-line, or via its graphical interface.
Simple usage
The recommended usage for simple files is one of the following lines:
frama-c file.c -<plugin> [options]
ivette file.c -<plugin> [options]
Where -<plugin>
is one of the several Frama-C plug-ins, e.g. -eva
, or -wp
, or -metrics
, etc. Plug-ins can also be run directly from the graphical interface, ivette
. A legacy version of the GUI (frama-c-gui
) is also available.
To list all plug-ins, run:
frama-c -plugins
Each plug-in has a help command (-<plugin>-help
or -<plugin>-h
) that describes its own options.
Finally, the list of options governing the behavior of Frama-C's kernel itself is available through
frama-c -kernel-help
Complex scenarios
For complex usage scenarios (several files and directories, preprocessing directives, etc), we recommend the following two-step approach:
Parsing the input files and saving the result to a file;
Loading the parsing results and then running the analyses or the GUI.
Parsing complex C applications usually involves C preprocessor options (e.g. GCC's -D
and -I
). In Frama-C, they are passed via option -cpp-extra-args
, as in this example:
frama-c *.c -cpp-extra-args="-D<define> -I<include>" -save parsed.sav
The results can then be loaded into Frama-C for further analyses or for inspection via the GUI:
frama-c -load parsed.sav -<plugin> [options]
ivette -load parsed.sav -<plugin> [options]
Further reference
Links to user and developer manuals, Frama-C archives, and plug-in manuals are available at
https://frama-c.com/html/get-frama-c.htmlThe Frama-C documentation page contains links to all manuals and plugins description, as well as tutorials, courses and more.
StackOverflow has several questions with the
frama-c
tag, which is monitored by several members of the Frama-C community.The Frama-c-discuss mailing list is used for announcements and general discussions.
The Frama-C blog has several posts about new developments of Frama-C, as well as general discussions about the C language, undefined behavior, floating-point computations, etc.
The Frama-C public repository contains a daily snapshot of the development version of Frama-C, as well as the issues tracking system, for reporting bugs. These contribution guidelines detail how to submit issues or create merge requests.
Dependencies (18)
-
conf-gtksourceview3
os != "macos" & os-family != "windows"
-
lablgtk3-sourceview3
os != "macos" & os-family != "windows"
-
lablgtk3
>= "3.1.0" & os != "macos" & os-family != "windows"
-
ppx_deriving_yaml
>= "0.2.0"
- ppx_deriving_yojson
- ppx_deriving
-
zarith
>= "1.9"
-
yaml
>= "3.0.0"
-
unionFind
>= "20220107"
-
ocamlgraph
>= "2.0.0"
-
ocaml
>= "4.13.1"
-
menhir
>= "20181006" & build
-
conf-graphviz
post
- alt-ergo
- alt-ergo-free
-
dune-site
>= "3.7.0" & != "3.13.0"
- dune-configurator
-
dune
>= "3.7.0" & != "3.13.0"
Dev Dependencies (5)
-
yojson
>= "1.6.0" & (>= "2.0.1" | !with-test)
-
why3
>= "1.7.1" & (< "1.8.0" | !with-test)
-
odoc
with-doc
-
ocamlgraph
with-test & >= "2.1.0"
-
conf-time
with-test
Used by (6)
-
frama-c-lannotate
>= "0.2.3"
-
frama-c-luncov
>= "0.2.1"
-
frama-c-metacsl
= "0.7"
-
frama-clang
= "0.0.16"
-
pilat
< "1.2" | >= "1.6"
-
why
< "2.32"