Frama-C is a platform dedicated to the analysis of source code written in C.
Frama-C has moved its official repository to our self-hosted Gitlab instance.
Official releases (starting from Frama-C 21) will no longer be updated here.
Nightly snapshots are also available in our Gitlab! You can now get access to the latest development version at: https://git.frama-c.com/pub/frama-c/-/tree/master
The official Frama-C issue tracker is now at our Gitlab: https://git.frama-c.com/pub/frama-c/-/issues
You can submit issues and pull requests using your Github login (choose "Sign in with Github" when prompted).
See you there!
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:
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.
For more detailed information about installing OPAM/Frama-C, see INSTALL.md.
Frama-C is available through OPAM, the OCaml Package Manager. This is the preferred installation method. Be sure to install opam v2.0 or higher. Then the following sequence of commands should install frama-c and its gui:
opam init
opam install depext
opam depext frama-c
opam install frama-c
Frama-C is developed mainly in Linux, often tested in macOS (via Homebrew), and occasionally tested on Windows (via the Windows Subsystem for Linux).
Frama-C can be run from the command-line, or via its graphical interface.
The recommended usage for simple files is one of the following lines:
frama-c file.c -<plugin> [options]
frama-c-gui file.c
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 GUI.
To list all plug-ins, run:
frama-c -plugins
Each plug-in has a help command
(-<plugin>-help
or -<plugin>-h
) that describes its several
options.
Finally, the list of options governing the behavior of Frama-C's kernel itself is available through
frama-c -kernel-help
For more complex usage scenarios (lots of files and directories, with several preprocessing directives), we recommend splitting Frama-C's usage in two parts:
Parsing typically involves giving extra arguments to the C preprocessor,
so the -cpp-extra-args
option is often useful, as in the example below:
frama-c *.c *.h -cpp-extra-args="-D<define> -I<include>" -save parsed.sav
The results are then loaded into Frama-C for further analyses or for inspection via the GUI:
frama-c -load parsed.sav -<plugin> [options]
frama-c-gui -load parsed.sav -<plugin> [options]
Links to user and developer manuals, Frama-C archives,
and plug-in manuals are available at
http://frama-c.com/download.html
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 official bug tracking system can be used for bug reports.
The Frama-C wiki has some useful information, although it is not entirely up-to-date.
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 Github snapshot repository contains the .tar.gz archives of stable Frama-C releases, ready to be cloned. It can also be used for reporting issues and submitting pull requests.