(kindly reviewed by T. Antignac, D. Bühler and F. Kirchner)
Among Frama-C 16 Sulfur's new features, one of them is dedicated to help setting up and iterating case studies. In this series of posts, we will explain how to use such scripts to save time when starting a new case study with EVA.
In this first part, we will explore the basics of the
framework and its use on an open source project. We will see how to get the
preprocessor flags needed to prepare an analysis template. This template is
in fact a Makefile which will be used to set up the analysis. It will enable us
to define the sources to parse by editing its targets.
In the next post, we will see that, once the set-up is done, the analysis steps are similar to the ones presented in previous EVA tutorials: run a simple analysis, then refine, improve the precision, iterate. Once an analysis has been run, we will see how to track red alarms to improve the coverage. This will lead to some syntactic fixes that will allow the analysis to go further.
The release 16 (Sulfur) of Frama-C includes a small set of files, called analysis scripts, whose purpose is to help starting new analyses with Frama-C. It is currently focused on analyses with EVA, but other plug-ins such as WP and E-ACSL may incorporate it as well.
The new files are available in the
analysis-scripts of Frama-C's
frama-c -print-share-path to obtain its exact location.
This directory currently contains a README, two small Bash scripts and a
frama-c.mk) which contains the bulk of it.
fcscripts, the old name of this set of files
(it was already being used by the
Git repository, under that name, but now it is part of the Frama-C release).
The upcoming Frama-C release will update that.
analysis-scripts relies on some GNU-specific, Make 4.0+ features. This version
of Make (or a more recent one) is already available on most Linux distributions
and on Homebrew for MacOS, but in the worst case, downloading and compiling
GNU Make from source should be an option.
Basically, what these files provide is a set of semi-generated Makefile targets and rules that automate most of the steps typically used by Frama-C/EVA developers to set up a new case study. The scripts themselves are extensively used in the open-source-case-studies repository, which serves as use example.
We start by cloning the repository1:
git clone email@example.com:GHamrouni/Recommender.git
1 Note: at the time of this posting, the latest commit is 649fbfc. The results presented later in this tutorial may differ in the future. You can select this commit via
git checkout 649fbfcin case this happens.
Then, inside the newly-created
Recommender directory, we look for its
build instructions. Many C open-source libraries and tools are based on
autoconf/configure/make, which may require running some commands before all
headers are available (e.g.,
./configure often produces a
config.h.in template). Frama-C does not require compiling the sources,
so in most cases you can stop before running
make. However, since Frama-C
does require preprocessor flags, you can use existing Makefiles to cheaply
obtain that information.
In order to find out which preprocessor flags are needed for a given program,
you can use tools such as CMake or Build EAR
to produce a JSON compilation database,
compile_commands.json. This is a JSON file which contains the
list of commands (including all of their arguments) to be given to the compiler.
It contains many options which are irrelevant to Frama-C (such as warning and
optimization flags, typically
-O), but it also contains preprocessor
-D, which we are interested in.
compile_commands.json file can be produced as follows:
If the project is based on CMake, add
cmakecommand-line, e.g. instead of
cmake <source dir>, use
cmake <source dir> -DCMAKE_EXPORT_COMPILE_COMMANDS=ON.
If the project is based on Makefile, use Build EAR. After Build EAR is installed, you just have to prefix
bear makeis usually enough to obtain the JSON database.
Note: Frama-C 17 (Chlorine) includes option
-json-compilation-database, which allows using
compile_commands.jsondirectly, rendering the next step unnecessary.
Once you have the file, simply grep it for
-D flags, e.g:
grep '\-I\|\-D' compile_commands.json
Those flags should be added to the preprocessor flags in Frama-C's Makefile
(described in the next section),
Note that these recommendations may not work in complex setups. Manual inspection of the commands used during compilation might be necessary to obtain all necessary flags.
We will create a Makefile for Frama-C, to manage dependencies and help re-run
analyses. In order to avoid having to type
make -f <name> each time,
we will name it
GNUmakefile, for the following reasons:
GNU Make gives preference to
Makefileif both exist, so the default file used when typing
makewill be ours, even if the project already has its own Makefile;
This avoids having to rename/overwrite existing makefiles (or, worse, having Frama-C's Makefile erased when re-running
analysis-scriptsMakefile already relies on some features specific to GNU Make, so there is no compatibility downside here.
If you want to name your Makefile otherwise, just remember to always add
-f <your makefile name> to the make commands presented in this tutorial.
GNUmakefile will be created with content based on the
template available on Frama-C's Github repository.
In this tutorial, we consider that Frama-C is installed and in the
to keep the template concise.
include $(shell frama-c-config -print-share-path)/analysis-scripts/frama-c.mk # Global parameters CPPFLAGS = FCFLAGS += EVAFLAGS += export FRAMA_C_MEMORY_FOOTPRINT = 8 # Default targets all: main.eva # Input files main.parse: <TO BE COMPLETED>
The essential element to complete this template is the list of files
to be parsed. Other arguments, such as flags for the C preprocessor
CPPFLAGS), for the Frama-C kernel (
FCFLAGS) and for the EVA plug-in
EVAFLAGS) are also to be filled by the user, when necessary.
Finally, note that the target name (
main) is completely arbitrary. You
can have multiple targets if your code contains multiple
The important part is the use of the suffixes
are hard-coded in the
analysis-scripts' Makefile to generate targets with
the appropriate dependencies and rules.
.parse suffix is used by
analysis-scripts to set the list of source
files to be parsed. It is associated to an
.eva target which runs the
EVA analysis. This target is generated by
analysis-scripts itself; we just
need to tell the Makefile that it should be run when we run
all is the first rule in our Makefile.
The list of source files to be given to Frama-C can be obtained from the
compile_commands.json file. However, it is often the case that the software
under analysis contains several binaries, each requiring
a different set of sources. The JSON compilation database does not map the
sources used to produce each binary, so it is not always possible to entirely
automate the process. You may have to manually adjust the sets of files to be
given to Frama-C. For a whole-program analysis with EVA, in particular, you
might want to ensure that there is exactly one file defining a
In the case of Recommender, since it is a library, the
src directory does not
main function. However, the
test directory contains two files,
each of them defining a
main function. In this tutorial, we will use the
test.c file as the main entry point of the analysis. We could also have used
-lib-entry option on one or more functions in the library. More advanced
users of Frama-C may prefer this option though we will keep it simple and use
the main function in
test.c as unique entry point in this tutorial.
Therefore, the list of sources to be filled in the
is the following:
main.parse: src/*.c test/test.c
We can test that Frama-C is able to parse the sources:
If you are strictly following this tutorial, you should have the following error:
[kernel] Parsing test/test.c (with preprocessing) test/test.c:1:25: fatal error: recommender.h: No such file or directory #include "recommender.h" ^ compilation terminated.
This is because we never included the actual
-I lines that we found in the
compile_commands.json file. Note that they include flag
which is relative to one of the subdirectories in
tools/*. Since our Makefile
(and thus Frama-C) will run relative to the base directory in
the actual include directive needs to be
-Isrc, which we add to
make main.parse now should succeed. Run it again. You will notice
that nothing is done: thanks to the dependencies managed by
unless you modify one of the source files, or the flags given to Frama-C
FCFLAGS), Frama-C will not waste time reparsing the results:
they have already been saved inside the
analysis-scripts will create a corresponding
directory with several files:
command: the command-line arguments used by Frama-C;
framac.ast: the pretty-printed normalized AST produced by Frama-C;
stats.txt: performance information (user time and memory consumption);
warnings.log: warnings emitted during parsing;
framac.sav: a Frama-C save file (a binary) with the result of parsing;
parse.log: the entire log of the parsing (includes the warnings in
All of these files are used internally by the analysis scripts or some other tools (notably for regression testing and profiling purposes), however only the last 2 files are occasionally relevant for the end user:
framac.savcan be used with
frama-c -load, for instance when trying different plug-ins;
parse.logcontains a copy of all messages emitted during parsing.
If we want to load the parsed files in the Frama-C GUI, we can use either
frama-c -load framac.sav, or more conveniently,
The advantage of the latter is that it will generate the
if it has not been done already.
This concludes the first part of this tutorial. In the next post, we will run EVA using our Makefile, then iterate to improve the analysis.