Analysis scripts: helping automate case studies, part 1André Maroneze - 25th Jan 2018
(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
analysis-scripts 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
share directory. Use
frama-c -print-share-path to obtain its exact location. This directory currently contains a README, two small Bash scripts and a Makefile (
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 open-source-case-studies 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.
Using analysis scripts
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 file from 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.
Obtaining preprocessor flags from a
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, commonly called
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 flags, mostly
-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.
Preparing an analysis template
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 (update: previously) available on Frama-C’s Github repository. (update: The template is now distributed with Frama-C).
In this tutorial, we consider that Frama-C is installed and in the
PATH 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
main functions. The important part is the use of the suffixes
.eva, which 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
make all, or simply
all is the first rule in our Makefile.
Setting sources and testing parsing
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 contain a
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 the
-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
main.parse target 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
-I../../src/, 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
Recommender, 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
analysis-scripts, 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
Contents of 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,
make main.parse.gui. The advantage of the latter is that it will generate the
.parse directory 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.