Setting up an analysis with the help of frama-c-script
By André Maroneze on Wednesday, January 16 2019, 12:00 - Permalink
Frama-C 18 (Argon) includes a new command,
frama-c-script, which contains a
set of helpful scripts for setting up new analyses. The available commands
will likely expand in the future. We present here a quick overview of how to
use them efficiently for a very fast setup.
frama-c-script is not a Frama-C plugin, but a command that is installed along
frama-c-gui, starting from version 18.0 (Argon).
frama-c-script on your terminal will output its usage messsage, which
includes the list of available commands (which may change in the future):
usage: frama-c-script cmd [args] where cmd is: - make-template [dir] Interactively prepares a template for running analysis scripts, writing it to [dir/GNUmakefile]. [dir] is [.] if omitted. - make-path [for Frama-C developers and advanced users without Frama-C in the path] Creates a frama-c-path.mk file in the current working directory. - list-files [path/to/compile_commands.json] Lists all sources in the given compile_commands.json (defaults to './compile_commands.json' if omitted). Also lists files defining a 'main' function (heuristics-based; neither correct nor complete). - flamegraph <flamegraph.txt> [dir] Generates flamegraph.svg and flamegraph.html in [dir] (or in the FRAMAC_SESSION directory by default). Also opens it in a browser, unless variable NOGUI is set.
These commands are often related to the analysis scripts described in
previous blog posts,
frama-c-script facilitates the usage of
but it also has commands which do not require them.
Each command is actually a script in itself, and may thus require other interpreters (e.g. Python or Perl).
The diagram below illustrates where
frama-c-script participates in the
workflow of an analysis: in the creation of a makefile template, and also
after the analysis, for profiling. Both usages will be detailed in this post.
frama-c-script is ideally used in conjunction with a
JSON compilation database.
As described in a previous blog post,
CMake, Build EAR or other tools can be used to produce a
file, containing the list of compilation commands along with their arguments.
Once you have a
compile_commands.json file, run:
It will parse the file and list all sources in it, in a Makefile-compatible
syntax. It will also output the list of files containing definitions for a
main function. This typically includes the main application itself, but also
test cases or secondary applications, which can all be useful entry points for
an analysis with Eva.
frama-c-scriptdoes not parse the source files to find function definitions; instead, it uses regular expressions to identify likely definitions, which can give both false positives and false negatives. This is a necessary approach since, during this stage, it is too early to have a full, parsable AST to begin with.
With the list of source files, we can now easily create a Makefile template for
our application. The
make-template command will interactively create a new
GNUmakefile in the current directory, after asking for some data:
- Name of the main
- List of source files.
The name of the main target is usually the application name. It is also the default Makefile target and the prefix of the directories where the results will be stored (both for parsing and for the analysis with Eva).
The list of source files can be as simple as
*.c, or more sophisticated for
projects with subdirectories and multiple
main functions, in which case some
source files must not be included in the list. The
will produce the list of sources when a
compile_commands.json file is present.
After these values are filled in, the script will create a
the current directory. The values are simply written inside the makefile to
help kickstart it, but they can be manually edited afterwards.
Ideally, this should be enough to try parsing the source files by running simply
make. From then on, the analysis-scripts methodology takes over, and the
usual commands (
make gui) work as usual.
One of the options in
frama-c-script is related to flamegraphs.
are stack trace visualizations which, in Frama-C/Eva, are used to help
understand in which functions the analysis spends most of its time.
-eva-flamegraph has been added in Frama-C 14 (Silicon),
and it activates the generation of a flamegraph trace file during the analysis.
This file can then be given to the
flamegraph.pl Perl script developed by
Brendan Gregg to produce an image in SVG format.
The image below provides an example of a flamegraph for the PolarSSL code in
repository. The stacks start from the top, with the
main function, and then
each called function is stacked underneath. The length of the bar is the amount
of time spent in it. Hovering over a bar shows the function name and the
percentage of time spent in the function. Clicking on a bar will zoom on it,
increasing the size of its children for better readability.
Note that bar colors do not have any special meaning.
flamegraph command available in
frama-c-script is simply a shortcut to
help generate the image file for the flamegraph (along with an HTML wrapper)
and open it in a browser. The
flamegraph.pl script itself is distributed in
share directory, which simplifies its usage.
analysis-scripts options already include the generation of
flamegraphs by default (option
-eva-flamegraph is set by
FRAMAC_SHARE/analysis-scripts/frama-c.mk), the user simply needs to run:
frama-c-script flamegraph <target>.eva/flamegraph.txt
And the user's default browser should display the flamegraph generated during the analysis.
Note that flamegraphs can be generated while the analysis is still running;
this is useful, for instance, when the analysis is seemingly "frozen" in a
given point, without emitting any messages. Running
will create a flamegraph of the current state of the analysis, while the
trace file is still updated by the ongoing analysis.
The features currently available in
frama-c-script offer extra comfort when
setting up new analyses, by minimizing the amount of repetitive or
list-files requires a JSON compilation database, but it helps obtain
the information for creating a GNUmakefile.
make-template creates a
GNUmakefile which can be manually edited later.
flamegraph helps visualize
the performance of the analysis, either while it is running, or afterwards.
One of the new commands expected for Frama-C 19 (Potassium) will help find
which files in a directory declare and/or define a given function. This will
help, for instance, when trying to identify which
.c file to include to
obtain the body of a function that is called from another source.