Setting up an analysis with the help of frama-c-scriptAndré Maroneze - 16th Jan 2019
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.
Presentation of frama-c-script
frama-c-script is not a Frama-C plugin, but a command that is installed along with
frama-c-gui, starting from version 18.0 (Argon). Running
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, but independent;
frama-c-script facilitates the usage of
analysis-scripts, 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).
Standard usage of frama-c-script
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
compile_commands.json 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
list-files command 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
GNUmakefile in 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.
Easily visualizing flamegraphs
One of the options in
frama-c-script is related to flamegraphs.
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. Option
-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 Frama-C’s open-source-case-studies 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 the Frama-C
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
frama-c-script flamegraph 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 hard-to-memorize tasks.
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.