Wednesday, October 2 2019

SATE VI Workshop: Frama-C satisfies the Ockham Criteria

During the SATE VI Workshop, organized by the NIST SAMATE project, Frama-C was confirmed as having satisfied the Ockham criteria for sound analysis tools. Frama-C previously satisfied the SATE V Ockham criteria (2013-2016) and found hundreds of errors in the test material.

We reported in this blog about our analysis of SATE VI's Juliet 1.3 test suite. The code is available on Github, so that anyone can install Frama-C and reproduce the results.

In this post, we summarize some of the discussions that took place during the workshop, including future directions for SATE VII.

The SATE VI Workshop took place at MITRE who are responsible, among other things, for the Common Weakness Enumeration, and focused mostly on the Classic track, which had the most tools participating in. With Frama-C, we briefly examined part of the DARPA CGC test suite, one of the code bases available for SATE 6 Classic, finding some unintentional bugs.

The official report is still being finalized, but a few interesting points could be observed from the presentations and discussions:

  • The Wireshark code base was a bit too large for some tools, while the SQLite code base seemed to hit a sweet spot between code size and bug complexity.
  • The bugs injected via GrammaTech's Bug Injector tool were not as diverse as one might expect, but nevertheless it managed to insert bugs that were able to discriminate sufficiently between tools. That is, if the bugs were "trivial" or "impossibly hard", then either all or none of the tools would have found them; instead, there was a wide distribution between tools.
  • Some tools had issues mapping the results to the locations expected in the test oracles, either because some oracles were no longer up-to-date, or because each tool's definition of sinks and sources (the lines in the code where bugs manifest themselves, and those in which the bug is actually present) were not necessarily identical to the expected ones.
  • Several tools ended up finding more bugs than the injected ones, which is not surprising given the size of the code bases.
  • The SARIF format will be the default (and likely only) format for SATE VII. This should minimize the time necessary for NIST to process the results. All present tool developers were either already SARIF-compatible, or intended to become in the nearby future (including Frama-C).
  • Besides Frama-C, Astrée participated in the Ockham track, and also satisfied the criteria. A few other tools also participated, but some details were still being discussed. Overall, at least 4 tools participated in the Ockham track, which is a progression from the previous edition. We see this as a positive evolution of the importance of sound analyses.

Overall, the tool exposition workshop was very informative, and we thank NIST for meeting the challenges of organizing it, including very extensive and helpful feedback.

The visibility offered by SATE helps tool developers to showcase their work, and allows users to obtain important feedback about them. Incorporating a static analysis tool in a development toolchain has a cost, but may bring considerable benefits; being able to better estimate this trade-off is an important outcome of NIST team's work.

Friday, June 7 2019

Habemus Frama-C in Fenestris (Frama-C on Windows, with WSL)

We have successfully compiled and tested the beta release of Frama-C 19 (Potassium) in the WSL (Windows Subsystem for Linux), using Debian. Installation is not trivial, especially for the graphical interface, but in the future this should provide a more robust way to run Frama-C on Windows, than relying on Cygwin/MinGW.

WSL + Cygwin/X

In a future post, or if there are explicit demands about the details of the installation procedure (for instance, via the frama-c-discuss mailing list), we may detail the whole process.

The main objective of this post is to (1) confirm to potential users that it is possible to install and run Frama-C using the Windows Subsystem for Linux and opam, and (2) inform that the WSL is likely a more efficient and robust solution than installing Cygwin and then opam on Windows from there. In our tests1, WSL was faster to compile Frama-C and its dependencies, and required less workarounds. The major pain point was the graphical interface (which required the installation of a separate X server), but after the initial setup, the GUI seemed to run smoothly.

1 None of the main Frama-C developers currently use Windows. What we could measure is that, between Cygwin on a Windows VM, and WSL on a Windows VM, the latter is much faster. We believe this remains true when running Windows natively.

Overview of the installation procedure

We used a Windows 10 Professional for the test. After enabling WSL, we installed Debian via the Windows Store, then some essential packages via apt (m4, curl, bzip2, and a few others), and installed opam 2 using the procedure based on curl. Note that using the opam package from Debian does not work, since it corresponds to opam 1.2. An upcoming Debian release will likely include opam 2, simplifying the procedure.

After installing opam 2 and configuring it without sandboxing (e.g. opam init --disable-sandboxing), which does not work on WSL, we installed a suitable OCaml compiler (4.07.1). We pinned the latest Frama-C Github release as indicated in the beta release e-mail:

opam pin add frama-c ""

Then, we installed depext and ran opam depext frama-c, to get all of its dependencies. After installing a few more Debian packages and then opam packages, Frama-C was installed and could be run using the command line.

Graphical apps on WSL require some effort

Frama-C without its GUI is only half the fun. In order to get frama-c-gui fully working, we had to install an X server, since WSL does not currently provide one. One such server is Cygwin/X, which requires installing Cygwin and then a few packages such as xorg-server and xinit. Instructions are available with helpful screenshots, but for those not used to Cygwin, the procedure is somewhat cumbersome.

In our tests, we used SSH with X forwarding enabled (installing openssh-server and configuring /etc/ssh/sshd_config), then ran the XWin Server shortcut created by Cygwin/X, opening an xterm, connecting via SSH (with -Y) to the WSL Debian instance, and running frama-c-gui from there. This step definitely needs some polishing for a simpler installation procedure. But, for now, it suffices to know that it is possible to use the Frama-C GUI in Windows.


WSL is a good alternative for those wanting to try Frama-C on a Windows installation. A Linux virtual machine is still a more robust and accessible solution, which works with older versions of Windows, but for a more lightweight and performant experience, WSL already allows using Frama-C.

Contact us or send a message to frama-c-discuss if you would like more detailed instructions about installing Frama-C with WSL.

Tuesday, February 26 2019

Finding unexpected bugs in the DARPA CGC corpus

Recently, we've been running Frama-C/Eva on the DARPA challenges from the SATE VI Classic track tool evaluation, organized by NIST. The C programs come from a Linux-compatible port of the DARPA Cyber Grand Challenge. The port was made by Trail of Bits and used as one of the evaluation sets of SATE VI.

These challenges contain each one or more bugs which lead to exploitable vulnerabilities. One of the goals of the Cyber Grand Challenge was to benchmark tools which should be able to automatically identify and patch these vulnerabilities.

However, given the amount of programs (over 240) and the number of lines of code (over 5 million LoC; this includes large tables of initializers and multiple copies of standard library functions, but it is nevertheless an impressive amount of code), the results were not entirely unexpected: Frama-C/Eva managed to find some cases of undefined behavior which were not listed as intentional bugs by the authors. In this post, we report some of these bugs, not all of which are currently detected by sanitizers (such as GCC's and Clang's) or Valgrind.

Normalizing the CGC challenges

The challenge set contains code written by several different companies (Kaprica Security, Cromulence, Narf Industries, and others). Each challenge is mostly independent of external libraries: functions such as strlen and malloc are defined in the lib directory of each challenge. One of the consequences of this fact is that the functions have slight variations in their signatures: some follow the C standard, while others replace void* with char*, or omit the const qualifier. Input/output functions, such as receive_* and transmit_*, contain a large amount of variants, which differ in number and order of arguments.

All of these facts make it more difficult to apply a uniform and generic wrapper for all challenges, to automate their testing with Frama-C/Eva. For maximal precision in the analysis, Eva uses its own built-ins for functions in string.h and stdlib.h. However, since each challenge includes its own version of the C standard library, with varying function signatures, an automatic replacement of all these functions with a simple set of stubs is not easy; in some cases, the files will not parse, for instance when a function has the same name as another but differs in the number of arguments.

This normalization phase involved some manual work, by tring to parse each challenge and using generic stubs/wrappers when possible, fixing issues on a case-by-case basis.

Some challenges use non-standard C language extensions, such as Clang's block extension, structs containing other structs which themselves contain flexible array members, or arithmetic operations with void pointers. In some cases, it is easy to patch them (e.g. by adding non-void* casts), but in others, such as the block extension, the transformation is not so straightforward. A few tests were not analyzed due to these syntactic deviations.

Finding the low-hanging fruit

By using Frama-C's analysis scripts, creating a generic Makefile, and some stubs for libc functions, we were able to start analyzing the CGC challenges in search of definitive problems (typically, red alarms in the GUI). Some of them are the "typical" causes of undefined behavior that go unnoticed in most cases: logical shifts of negative numbers; and access of uninitialized variables. The former is usually deterministic for a given architecture (although non-portable, and not future-proof: a new version of a compiler may change the behavior), but the latter can lead to nondeterministic problems.

Other cases of (unintended) undefined behavior found in the challenges include off-by-one errors (incorrect loop conditions, or memory allocation for a string which does not include the terminating NUL byte), conditions in the wrong order (e.g. dereferencing an array element before checking if the index is in range) and double free. A summary of findings is available at the Github open source case studies wiki. It will be updated when there are new findings.

Almost all of the cases can be easily fixed once the issue is detected. The Frama-C GUI allows navigating between callers, filtering call stacks, and providing context information to identify the origin of the issue. Once it is fixed, re-running the analysis confirms the issue is resolved, and Eva is able to advance further in the program execution. In one case, fixing an issue revealed a second one later in the analysis.

Sanitizers help, but not always

Sanitizers can be used to help identify undefined behavior, but they are not always sufficient. Even when execution is not dependent on input data (e.g. during initialization), and therefore the undefined behavior is always triggered, several conditions may affect whether sanitizers will detect them.

For instance, in Square Rabbit (a program which simulates a Blackjack-style card game), the user gives inputs such as "H"(it) or "S"(tay), and the amount money to bet, and the program simulates a random deck of cards, a dealer, and tracks the amount of money the player has.

The injected vulnerability in this test concerns a counter related to the number of split hands, which overflows and leads to a crash. However, it turns out that the readline function used in this program has an undocumented issue: whenever the input buffer is full (i.e., the user sent 512 characters or more in a single line), there is an access to the byte just after the last one in the array:

static int readline(int fd, char *buf, size_t size)
  size_t i;
  size_t rx;

  for (i = 0; i < size; i++) {
    if (receive(fd, buf, 1, &rx) != 0 || rx == 0)
    if (*buf == '\n')

  if (i == size && *buf != '\n') // <<< accessing buf[512]
    return -1;
  else if (*buf != '\n')
    return 1;
    *buf = '\0';

  return 0;

When unrolling the loop in Frama-C/Eva (with a loop unroll annotation, for instance), and using option -eva-split-return, to ensure separation of states from the previously called functions, Eva is capable of inferring that, when the input has a line with 512 characters or more, the only way to enter the conditional after i == size is with a pointer to one-past the last element in the array. Thus, reading the byte at this position constitutes an undefined behavior, although unlikely to be exploited. Note that, if that character (which might be the first byte of the next variable declared in the stack, after the array) is a newline, then not only is this one-past element read, but it is also written to, replaced with \0.

As an exercise, we would like to reproduce this bug in an actual execution, using tools such as Valgrind and code sanitizers to instrument the code and obtain an assertion error when the memory is unduly accessed.

Runtime confirmation of undefined behavior using a sanitizer

Let us compile the code using Clang and AddressSanitizer:

clang -fsanitize=address -o square_rabbit src/*.c lib/*. -I. -Ilib

You may have to adapt your command line to ensure all required files are included, with the proper directives.

Then, let us provide some input that triggers the undefined behavior, containing a line larger than 511 characters. The following Python one-liner produces an input that starts a new game and then provides a line with just enough characters to trigger the buffer overflow:

python -c "print('39\n1'); print('A' * 512); print('1000\nS\nQUIT\n2\n')" | \

The above input will:

  • provide a random seed (39);
  • start a new game (option 1);
  • provide some useless input that overflows the buffer (512 A's);
  • play a game (1000/Stay/QUIT);
  • finally, quit the program (option 2).

If square_rabbit had been compiled without a sanitizer, it would just run normally, and the user would be unaware of the undefined behavior. But Address Sanitizer will detect the off-by-one error and stop the execution:

==20070==ERROR: AddressSanitizer: stack-buffer-overflow on address (...)

Address 0x7ffd436f5ca0 is located in stack of thread T0 at offset 544 in frame
    #0 0x511e7f in play_squarerabbit src/game_sultan.c:260

  This frame has 1 object(s):
    [32, 544) 'input' (line 265) <== Memory access at offset 544 overflows this variable

Valgrind can also detect some kinds of undefined behavior

Another tool that can help detect such issues is Valgrind. Running square_rabbit with our input (without instrumenting it with AddressSanitizer) will report the following:

==21267== Conditional jump or move depends on uninitialised value(s)
==21267==    at 0x401BBB: readline (game_sultan.c:73)
==21267==    by 0x401704: play_squarerabbit (game_sultan.c:255)
==21267==    by 0x401EAA: main (game_sultan.c:376)

The message is less precise than the one reported by AddressSanitizer, but it contains the essential information. For such a small piece of code, the overhead imposed by Valgrind is barely noticeable (0.2s instead of 0.05s).

In the heap, detection is not so easy

In both cases, we were somewhat "lucky" that the error was detected by the tools. Some minor changes, however, can make the error go unnoticed. For instance, if we move the declaration of the local buffer variable (char input[INPUT_SIZE]) to a global declaration, moving it from the stack to the heap, both tools fail to detect the off-by-one overflow.

That is, unless we include another modification: if we move input to become a global variable, and we add an initializer to it (even an initializer semantically equivalent to no initializer at all, such as = {0}), then AddressSanitizer is able to detect the overflow -- but not Valgrind. Your mileage may vary according to your compiler version, optimization flags, etc.

Overall, relying on sanitizers and/or Valgrind to identify undefined behavior is not the safest bet: first, they can only detect issues in the current execution, which might be input-dependent; second, even when undefined behavior is triggered, the memory layout of impacted variables may prevent these tools from detecting and reporting the issue.


The DARPA challenges provide a very interesting set of non-trivial C programs for code analyzers. Their inclusion in the SATE 6 Classic track is a good choice for evaluating bug finders. As expected for a code base of such size, there are a few cases of unintentional bugs that evaded testing. Using Frama-C/Eva to analyze these programs allowed the identification of some such bugs. We hope our online report of these findings should help the SATE team to address them in future versions of the tool evaluation. We also expect to include some of the challenge programs in our open source case studies suite.

Wednesday, January 16 2019

Setting up an analysis with the help of frama-c-script

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 and 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 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.

Integration of frama-c-script in the analysis workflow

Currently, 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:

frama-c-script list-files

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-script does 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 make target;
  • 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 parse, make, 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 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.

Eva flamegraph

The 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 script itself is distributed in the Frama-C share directory, which simplifies its usage.

Since the analysis-scripts options already include the generation of flamegraphs by default (option -eva-flamegraph is set by FRAMAC_SHARE/analysis-scripts/, 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.

Friday, December 14 2018

New loop unroll annotation in Frama-C 18

One of the new features in Frama-C 18 (Argon) is the annotation @loop unroll, used by the Eva plug-in to replace and improve upon the usage of slevel for semantically unrolling loops. This new annotation is more stable, predictable, and overall more efficient. In this post we present the annotation with some examples where it outperforms previous mechanisms.

Loop unrolling mechanisms in Frama-C/Eva

Frama-C has two ways to unroll loops syntactically: either via option -ulevel N (which unrolls all loops in the program N times), or via the loop pragma UNROLL annotation, placed before a loop, which unrolls only that loop. Both have their uses, especially for plug-ins other than Eva; however, Eva has specific mechanisms which are almost always better suited to deal with loops.

When using the Eva plug-in, syntactic loop unrolling is is not recommended: it is more costly than semantic unrolling, and it makes the code harder to read in the GUI.

In Eva, the slevel mechanism is used to improve precision of the analysis inside loops: as long as there is enough slevel to be consumed, each loop iteration will keep consuming it before performing a widening and merging states, which might lead to loss of precision.

This works fine for simple loops, but as soon as there are branches or nested loops, slevel consumption is hard to control: each branch will also consume some slevel, and there is no way to ensure that only outer loop iterations will consume the remaining slevel.

To mitigate the effects of unwanted slevel consumption, options such as -eva-slevel-merge-after-loop force the merging of states at the end of each loop iteration, which minimizes the issue with loops containing branches. However, this option operates at the function level, so nested loops are still an issue.

Plug-ins such as Loop Analysis perform complex estimations to try and indicate values of slevel for each function, accounting for the fact that nested loops and branches require extra slevel. In realistic code bases, this often leads to functions having excessively large values of slevel (in the worst case, such overflows lead to 0, that is, giving up unrolling).

In the end, existing solutions had drawbacks which imposed an extra burden on the parameter refinement process. This motivated the development of the new @loop unroll annotation.

The new loop unroll mechanism

@loop unroll N is a code annotation, to be placed just before a loop in the program (as is the case with all @loop ACSL annotations). It will instruct Eva to avoid merging states after each loop iteration, until either:

  • there are no more states to unroll (i.e. the loop has been completely unrolled), or

  • N unrollings have been performed.

Just like with slevel, a value for N larger than the required to completely unroll the loop will not lead to wasted time.

The annotation currently accepts only constant expressions, that is, those involving literal constants or #define macros. This limitation may be removed in the future.

Nested loops and slevel usage

The main advantage of using @loop unroll is in the presence of nested loops. Consider the following example:

void main() {
  int a[10][10] = {0};
  for (int i = 0; i < 10; i++) {
    for (int j = 0; j < 10; j++) {
      a[i][j] += i + j;

In this program, one might naively think that using -eva-slevel 100 would be enough to unroll the loops. This will however result in:

[eva] example1.c:4: starting to merge loop iterations
[eva:alarm] example1.c:5: Warning:
  signed overflow. assert a[i][j] + (int)(i + j) ≤ 2147483647;
[eva:final-states] Values at end of function main:
   [8][9] ∈ {17}
   [9][0] ∈ {9}
   [9][1..9] ∈ [0..2147483647]

The first message indicates that there was not enough slevel to consume during the analysis, and thus a merge between different loop iterations happened, resulting in loss of precision. Widening causes the last cells of the matrix to contain over-approximated intervals, leading to an alarm.

The reason why 100 is not enough is due to the fact that an extra slevel is consumed for each iteration of the outer loop; for instance, you can try using -eva-slevel 10 and then -eva-slevel 11 and checking the displayed final states: in the first case, the result remains imprecise for the entire matrix:

[eva:final-states] Values at end of function main:
  a[0..9][0..9] ∈ [0..2147483647]

While in the second case (-eva-slevel 11), we have:

[eva:final-states] Values at end of function main:
  a[0][0] ∈ {0}
   [0][1] ∈ {1}
   [0][2] ∈ {2}
   [0][3] ∈ {3}
   [0][4] ∈ {4}
   [0][5] ∈ {5}
   [0][6] ∈ {6}
   [0][7] ∈ {7}
   [0][8] ∈ {8}
   [0][9] ∈ {9}
   [1..9][0..9] ∈ [0..2147483647]

Thus, the actual slevel required to completely unroll both loops is 109 (the last iteration does not require extra slevel). Computing this exact value is not straightforward, and it gets even more complicated when there are branches in the loop.

Using @loop unroll in nested loops

The @loop unroll annotation is local to a loop, and thus completely independent of whether the loop contains or is contained by other loops. Therefore, we can perform simple calculations to obtain the bounds: (max - min) / step in the general case, which here results in (10 - 0) / 1 = 10.

void main() {
  int a[10][10] = {0};
  //@ loop unroll 10;
  for (int i = 0; i < 10; i++) {
    //@ loop unroll 10;
    for (int j = 0; j < 10; j++) {
      a[i][j] += i + j;

With the above annotations, simply running Eva, without any slevel required, will result in no alarms at all. The bounds are much simpler to compute. In future Frama-C releases, we hope to obtain this information automatically whenever possible, so the user will not have to add them in simple cases.

There is currently (in Frama-C 18 - Argon) an option to set a minimum value for @loop unroll for all loops in the program: -eva-min-loop-unroll. This may be unwise for realistic case studies with several loops, but in many cases this saves time by not having to add annotations to each loop in the program. In our first example, adding -eva-min-loop-unroll 10 has the same effect as adding the two //@ loop unroll 10; annotations.

Loops with branches and slevel usage

The previous example was comprised of two very simple nested loops. In reality, many loops contain branches and conditional exits. In such cases, slevel usage becomes exponential. For instance, consider this variant of the previous example, with a non-deterministic increment:

void main(int nondet) {
  int a[10][10] = {0};
  for (int i = 0; i < 10; i++) {
    for (int j = 0; j < 10; j++) {
      a[i][j] += i + j;
      if (nondet) a[i][j]++;

In this example, instead of 109 as minimum slevel to avoid any warnings, Eva needs 5509. On my machine, the analysis goes from nearly instantaneous (about 0.3s) to visibly perceptible (about 1.7s). And all this for a very modestly-sized loop, with a single branching point.

Eva has an option to help mitigate the issue with slevel: -eva-slevel-merge-after-loop <functions>. This option ensures that, at the end of each loop iteration, all states from different branches in the current iteration will be merged. This avoids the exponential explosion, but still requires extra slevel, in a non-intuitive manner; for instance, the minimum slevel value required to avoid warnings in the above example is 208. Simply trying to understand precisely why this value is necessary and sufficient requires deep understanding of the evaluation mechanism inside Eva.

Again, if we add the same @loop unroll annotations as before, we do not need anything else: the analysis will not generate any warnings, it will run almost as fast as before (with a barely perceptible increase in time due to the branching), and it will be robust to changes: the introduction of extra branches or nested loops will not affect the existing annotations.

Warnings to help the user

The message starting to merge loop iterations is used to indicate insufficient slevel during the analysis of loops. A more specific warning is now available for loop unroll annotations. For instance, suppose we used 9 instead of 10 in our previous annotations. Eva would then report:

[eva:loop-unrolling] example2.c:6: loop not completely unrolled

This warning appears when there is an annotation that is insufficient to completely unroll the loop, which is often a sign that the annotation should contain a larger value. It can be disabled or even turned into an error, to make sure the user will not miss it.

Upgrading to the new mechanism

Existing case studies may benefit from the new annotation without requiring changes to existing parametrization; in most cases, keeping current slevel values (which are still necessary for dealing with branches) while adding such annotations should give results at least as precise, possibly improving the efficiency of the analysis. Then, slevel values can be lowered on a second stage.

The analysis scripts and sources in the Github open-source-case-studies repository have been updated to include several loop unroll annotations throughout the code, to serve as usage examples. During the process, we could confirm their improved reliability, predictability and ease of use. Their only downsides are that some oracles change due to different line numbers after they are introduced, and the fact that some (if not most) of these annotations could be automatically generated.


The slevel mechanism is very generic, but not appropriate in all situations, especially because it does not allow fine-grained control, and is context-dependent. Having a specific mechanism for handling loops, which is the majority of practical use cases, improves reliability and predictability of the analysis. It also prevents exponential blowup of states in more complex loops.

loop unroll annotations are very useful and likely to be present in every meaningful case study. Their usage is straightforward, and future Frama-C versions may end up incorporating more flexible annotations (e.g. using non-constant expressions). The slevel mechanism is still used in some cases, especially for branching, but its usage is likely to diminish over time, replaced with more specialized and expressive mechanisms.

Thursday, November 15 2018

Frama-C/Eva in SATE VI with Juliet 1.3

Frama-C chose to participate in the SATE VI Ockham Sound Analysis Criteria. With the upcoming Frama-C 18 (Argon) release, results can be reproduced using the open source version of the Eva plug-in. This post briefly presents SATE, the Juliet test suite, and the results obtained with Frama-C 18. We then describe the Frama-C SATE VI repository on Github, created to allow anyone to reproduce the results obtained with Frama-C/Eva. We also explain some patches that were applied to the test suites, and our choice of parametrization options for Eva.

SATE VI and Juliet 1.3

SATE (Static Analysis Tool Exposition), organized by NIST, is a comparative study of static analysis tools: toolmakers volunteer to participate by running their tools on the sets provided by NIST, and then by submitting their analysis scripts and results. The NIST SAMATE team then compiles a dense report, comparing and evaluating all participating tools.

For the analysis of C programs, there are two tracks: one in which all kinds of tools participate, called the Classic track, and another dedicated to sound analyzers, in the sense of the Ockham Sound Analysis Criteria.

For the Ockham track in SATE VI, we chose the Juliet 1.3 test suite for C/C++, which contains over 64,000 test cases. Some are written in C++, but most are written in C. Test suites are organized in directories related to CWEs (Common Weakness Enumerations): each directory has code samples containing violations of the CWE. For each test case, there are two variants: one with good code (which does not trigger the CWE), and another with bad code (which triggers the CWE in question). In our tests using Juliet, Frama-C is supposed to find all occurrences of bad code; it may, however, report some good code as bad.

CWEs handled by Frama-C/Eva

For the analysis with Frama-C/Eva, we chose the subset of CWEs in Juliet 1.3 for C/C++ which are handled by the analyzer. Click the arrow below to unfold the list.

CWEs in Juliet 1.3 handled by Frama-C/Eva (18 - Argon)
  • CWE121 - Stack Based Buffer Overflow
  • CWE122 - Heap Based Buffer Overflow
  • CWE123 - Write What Where Condition
  • CWE124 - Buffer Underwrite
  • CWE126 - Buffer Overread
  • CWE127 - Buffer Underread
  • CWE190 - Integer Overflow
  • CWE191 - Integer Underflow
  • CWE194 - Unexpected Sign Extension
  • CWE195 - Signed to Unsigned Conversion Error
  • CWE196 - Unsigned to Signed Conversion Error
  • CWE197 - Numeric Truncation Error
  • CWE369 - Divide by Zero
  • CWE415 - Double Free
  • CWE416 - Use After Free
  • CWE457 - Use of Uninitialized Variable
  • CWE464 - Addition of Data Structure Sentinel
  • CWE469 - Use of Pointer Subtraction to Determine Size
  • CWE475 - Undefined Behavior for Input to API
  • CWE562 - Return of Stack Variable Address
  • CWE587 - Assignment of Fixed Address to Pointer
  • CWE588 - Attempt to Access Child of Non Structure Pointer
  • CWE590 - Free Memory Not on Heap
  • CWE617 - Reachable Assertion
  • CWE665 - Improper Initialization
  • CWE690 - NULL Deref From Return
  • CWE758 - Undefined Behavior
  • CWE835 - Infinite Loop
  • CWE843 - Type Confusion

Note that some CWEs are very broad, such as CWE758 - Undefined Behavior. We do not claim Frama-C/Eva handles all cases which might be categorized under such CWEs; however, those considered in the Juliet 1.3 test suite have all their bad code samples correctly labeled.

Some examples of CWEs which are not considered by Frama-C/Eva include CWE426 - Untrusted Search Path, CWE90 - LDAP Injection and CWE780 - Use of RSA Algorithm Without OAEP. All three of them constitute functional-level weaknesses which do not cause runtime errors.

Some of the CWEs not currently considered by Frama-C/Eva could be handled via specific function annotations, but this would constitute a very ad hoc solution. Other plugins in the Frama-C platform might be better suited for these CWEs; e.g., using the WP plugin with function annotations, or the Secure Flow plugin with trusted and untrusted sinks and sources, might allow identifying the cases with API violations leading to weaknesses.


The following table summarizes the results obtained with Frama-C 18 (Argon). The script that produces this table is presented in a later section.

total imprecise      :    751
total non-terminating:      3
total ok             :  44668
total timeout        :      0
total unsound        :      0
precision (excluding non-terminating): 0.983465

Each test case is labeled as one of the following cases:

  • ok: correctly labeled: either a good test without alarms, or a bad test with alarms;
  • imprecise: a good test with a false alarm;
  • unsound: a bad test without an alarm;
  • non-terminating: the program does not terminate; this should never happen, except in the case of CWE835 - Infinite Loop;
  • timeout: a test which did not finish within the allotted time (by default, 30 seconds). This never happens in our benchmarking rig, but slower or overloaded machines may see this happen. If so, then a larger timeout should be given and the test should be re-run.

The precision (98.3%) displayed in the last line is the number of ok tests divided by the total number of tests (ok + imprecise + unsound).

The improvements between Frama-C 17 (Chlorine) and 18 (Argon) are noteworthy, especially the fact that the memcpy and memset builtins are now released in the open source version. Other improvements in precision also contributed to remove some spurious warnings and to simplify the analysis script.

The remaining imprecisions are due to different situations, but most of them occur several times, due to reuse of the same patterns among different test cases. One source of imprecision is the snprintf function, whose specification is not precise enough to ensure that the output string is null-terminated. This leads to false alarms when that string is used later in the code. Another case is related to CWE369 - Divide by Zero, in which some tests use socket-related functions whose specifications do not allow for precise results in every case.

The Frama-C SATE VI Repository

The Frama-C SATE VI repository on Github allows anyone to run Frama-C on the Juliet 1.3 test suite for C/C++, to reproduce the results or to try different approaches, e.g. parametrizing the analysis differently, or trying a new abstract domain.

Software requirements are: Frama-C 18.0 (Argon), GNU Make (>= 4.0), the GNU parallel tool, Bash (>= 4.0) and wget (to download the Juliet archive from NIST's website).

The repository is structured in the following way:

  • A GNUmakefile allows bootstrapping the repository, by downloading the Juliet 1.3 for C/C++ archive from NIST's website and then decompressing it (Juliet 1.3 is not distributed in our repository). It also applies some patches to Juliet's sources, described in a later section;
  • the fc directory contains Frama-C scripts used to run the analysis and automatically evaluate its results. The main scripts are:
    • sets the default analysis parameters; these differ from Frama-C's defaults in several ways, being stricter in some cases but less strict in others;
    • performs automatic evaluation of good and bad cases into the categories presented before;
  • the fc/patches directory contains some patches applied to Juliet 1.3 to fix known issues in a few tests. It also changes the way non-deterministic random numbers are used in some tests (details are presented later);
  • the C directory contains the extracted Juliet 1.3 archive, with its scripts and test cases;
  • finally, the oracles directory contains a versioned copy of the oracles produced by the analysis with Frama-C/Eva; this allows comparing different parametrizations, and following the evolution of the platform.

Reproducing the results

The overall process to use the repository is the following:

git clone
cd C/testcases

The last make step takes a very long time (2+ hours, depending on your CPU and number of cores).

Note that, if Frama-C is not installed in the PATH, you can use the fc/ script to specify the directory where Frama-C is installed. This is especially useful to compare different versions of Frama-C.

After running make inside the C/testcases directory, a small summary with the number of tests performed in each subdirectory will be presented in textual form:

CWE121_Stack_Based_Buffer_Overflow/s01: 876 tests
    876  ok
CWE121_Stack_Based_Buffer_Overflow/s02: 1020 tests
   1020  ok
CWE121_Stack_Based_Buffer_Overflow/s03: 1020 tests
     34  imprecise
    986  ok

Running ./ will also output this result. The script will produce an overall summary across all subdirectories, as presented in the Results section.

Re-running individual tests

Inside each directory in C/testcases/, it is possible to run a single test, by removing its extension and adding _good.res or _bad.res, e.g. if there is a file file.c inside directory CWE000/s01, then doing cd CWE000/s01 and make file_good.res will run the test and produce three files:

  • file_good: output of the analysis;
  • file_good.csv: CSV report of warnings produced during the analysis;
  • file_good.res: result of applied to the test case report;

Note that for tests consisting of multiple files (each ending with a, b, c, etc.), the test case name is their prefix without the letter, e.g. for the test comprised of files file_42a.c and file_42b.c, the command is make file_42_good.res (or bad).

Finally, by replacing .res with .gui in the make command, it is possible to open the Frama-C GUI on the test case, to inspect it.

Patches applied to Juliet 1.3

In the Frama-C SATE VI repository, there are two sets of patches applied to Juliet 1.3 for C/C++:


These are fixes in a small number of tests, due to 2 patterns which were found out to lead to undefined behavior.

The first fix consists in replacing an overflow check which accidentally introduces a signed overflow:

 /* FIX: Add a check to prevent an overflow from occurring */
-if (abs((long)data) <= (long)sqrt((double)CHAR_MAX))
+if (data <= LONG_MAX && labs(data) <= (long)sqrt((double)CHAR_MAX))

data has type unsigned int. In the original code, the call to abs((long)data) is equivalent to abs((int)(long)data), since abs takes an int as argument. If int and long have the same length (e.g. as in x86 32-bit), then data can be larger than LONG_MAX (and also INT_MAX, since they have the same length), leading to a signed overflow in the call, and thus an undefined behavior. The patched version first checks that data is small enough, and then uses labs to avoid downcasting data.

The second fix concerns a set of files which had a local variable declared in a scope smaller than intended:

 static void goodG2B()
     void * data;
+    int intBuffer = 8;
     /* Initialize data */
     data = NULL;
     /* FIX: Point data to an int */
-        int intBuffer = 8;
         data = &intBuffer;
     CWE843_Type_Confusion__short_68_goodG2BData = data;

In this set of test cases, intBuffer (and similar variables) was declared inside a block, and the value was later used outside of the scope of the variable, leading to undefined behavior. The fix consists in declaring the variable in the main scope of the function.


This concerns mainly the RAND32 macro, used in Juliet to produce non-deterministic numbers. This macro is used in some test cases to assign values to variables of different types. The result is downcast to char or short whenever necessary. However, this downcast leads to warnings due to usage of option -warn-signed-downcast. This option is enabled in the script since some CWEs are related to it.

The patches applied to the test cases consist in replacing calls to (char)RAND32() and (short)RAND32() with RAND8() and RAND16(), two new macros defined in a way that prevents overflows from happening. These macros are defined in a way very similar to the existing RAND32() and RAND64() macros, but avoiding overflows triggering downcast warnings. To preserve existing behavior, these macros are defined to RAND32() when not running Frama-C.

Finally, minor patches were applied to pretty-printing functions in io.c, such as:

void printHexCharLine (char charHex)
-    printf("%02x\n", charHex);
+    printf("%02hhx\n", charHex);

The printf modifier for a variable of type char is hh, although this is very rarely used in practice. Still, the Variadic plug-in warns about it, so fixing the test case support file prevents spurious warnings.

Note that all of these patches are intended to improve the precision of the analysis, but do not affect its correction: not applying these patches will lead Frama-C/Eva to produce several spurious warnings (and, in a few cases, such warnings will lead to non-termination, when the only possible behavior is undefined), but their absence will not make Frama-C's results unsound; bad cases will still be reported as such.

Rationale for analysis options

The script contains a series of non-default options used in the analysis. We present here the rationale for choosing these options during the analysis of Juliet 1.3. Similar options are grouped together for presentation purposes.

-no-autoload-plugins -load-module from,inout,report,scope,eva,variadic

These options are present in most of Frama-C's test suites. The -no-autoload-plugins option simply disables by default all plugins, which speeds up initialization of Frama-C. We then only load the plug-ins which are needed for Juliet: eva and its derived plugins (from, inout, scope), report for the CSV report, and variadic to handle variadic functions present in almost every test (e.g. printf). Overall, this is an optimization for running thousands of tests; when running only a few dozens of tests, the difference is negligible.

-kernel-warn-key parser:decimal-float=inactive \
-kernel-warn-key typing:no-proto=inactive \
-kernel-warn-key typing:implicit-conv-void-ptr=inactive \
-eva-warn-key locals-escaping=inactive

These options disable warnings which are not directly related to runtime errors, but are enabled by default since they often indicate code quality issues in real code bases. The first three warnings could be avoided by patching the code (e.g. adding prototypes, explicit casts, and avoiding inexact floating-point constants); the latter is related to addresses of variables remaining accessible out of their scopes (in Eva, their value becomes ESCAPINGADDR), and it is emitted since it is often easier to identify the moment where the variable becomes out of scope, rather than the later time at which it may be used. This is not an undefined behavior, unless the variables are actually used (which does not happen in the good test cases). In any case, when the values are accessed (as in the bad test cases), a different warning is emitted.

-eva-msg-key=-initial-state \
-eva-no-show-progress \
-eva-print-callstacks \

These are all options related to minimizing the default verbosity of the analysis, except for the last, which adds callstacks to the output: when there are warnings, it is better to know where they come from.

-slevel 300 \

Some amount of slevel is useful to improve precision of the analysis. The chosen value is arbitrary, and variable according to the characteristics of the code under analysis. In the case of Juliet 1.3, this value is a good compromise between precision and speed of the analysis.

-eva-builtin alloca:Frama_C_vla_alloc_by_stack \

The alloca function (which is not in the C standard) is used in several test cases. In all of them, it behaves just like the allocation of a VLA (variable length array), that is, the variables are not used outside of the scope in which alloca was called1 . It is therefore safe to associate the vla_alloc builtin to calls to the alloca function in Juliet 1.3.

1 The main difference between alloca and the allocation of a VLA is that the latter is deallocated at the end of the scope in which it was created, while alloca memory blocks are deallocated at the end of the function in which they are called.

-warn-special-float none \

By default, Frama-C considers non-finite floating-point values as forbidden, emitting warnings when they may arise, even though this does not constitute an undefined behavior. This option allows non-finite floating-point values, thus avoiding spurious warnings.

-warn-signed-downcast \
-warn-unsigned-overflow \

Signed downcasts (possible loss of information when converting a larger type to a smaller one) and unsigned overflows, by default, do not constitute undefined behavior; however, it is a good practice to avoid them, and some specific CWEs do require treating them as undesired. Another option that could have been activated is -eva-symbolic-locations-domain, but in Juliet 1.3 it does not make any difference, neither in the oracles nor in the overall analysis time.

-eva-warn-copy-indeterminate=-@all \

By default, copying a possibly indeterminate value (e.g. uninitialized) in Eva triggers a warning, even if the value is copied in a standards-compliant way (e.g. via unsigned char pointers). This helps detect problems earlier in the code, rather than when used. However, the usage of such values already triggers warnings anyway, so we can afford to be less strict, avoiding spurious warnings in good test cases where the copied values are not used later.

-eva-equality-domain \
-eva-sign-domain \

These two abstract domains are efficient enough to be used in most analyses, and improve the precision of the results at a minimal cost. The equality domain in particular is useful in some tests which require relational information, while the sign domain is well suited for testing divide-by-zero errors. The equality domain eliminates false alarms in 184 tests, and the sign domain removes 308 false alarms.


This is a technicality, but useful for scripts and versioning: by default, Frama-C uses relative paths when they are "sufficiently close" to the current working directory, otherwise absolute paths are used (e.g. when there is a .. in the path). To avoid versioning such paths (and also for creating test oracles), Frama-C has a mechanism to replace specific paths with user-defined strings. The most common use case is Frama-C's share directory, written as FRAMAC_SHARE in reports and in the GUI. In this case, the actual path to the C/testcasesupport directory is replaced with string TESTCASESUPPORT_DIR. This ensures every user should have the same oracles for the CSV files mentioned below.

-report-no-proven -report-csv <file>.csv

These options are not present in, but in, due to availability of the output filename. These options invoke the Report plug-in to generate a CSV file containing the list of properties in the program, along with their statuses. Option -report-no-proven filters only the properties which are left Unknown or Invalid, which are the ones we are interested in when looking for undefined behaviors.


The NIST SAMATE Juliet 1.3 test suite for C/C++ provides an excellent set of well-defined programs, as well as programs with isolated bugs, which are very useful for automated testing and comparative evaluation.

Frama-C/Eva can handle several of the CWEs present in the test suite, and recent improvements in the analyzer allow it to obtain a very high precision. The tests cases are small, which does not make them representative of large case studies, but they allowed the identification of limitations in the analyzer and offered opportunities for improvement.

The analysis with Frama-C/Eva allowed the identification of very few issues with the code, which given the size of the test suites is an indicator of its high quality.

Overall, participation in the Ockham track enabled Frama-C/Eva to improve its analysis, and offered a very extensive set of test cases for regression testing and quantitative experimentation with different parametrizations. For instance, the sign domain, developed originally as part of a tutorial for Eva, proved itself very useful to improve the precision of several tests related to CWE369 - Divide by Zero, with a minimal runtime cost. The large-scale testing afforded by Juliet enables such kinds of evaluation.

We would like to thank NIST for preparing Juliet and organizing SATE, and for their commitment to the exposition of innovative tools for program analysis and verification.

Friday, July 6 2018

Parsing realistic code bases with Frama-C

A recurring subject when using Frama-C, especially intriguing for newcomers, is how to reach the stage where parsing of a realistic code base (as in, one that uses external libraries and compiles to different architectures) succeeds. This post will show a bit of the depth involved in the subject, presenting frequently encountered issues, and discussing some possible solutions, with varying trade-offs between short-term and long-term viability.

Frama-C parsing and external libraries

Most C software is non-portable, at least in the POSIX sense: usage of Linux-, BSD- or glibc-specific libraries is present in the majority of C code bases. This is not a huge issue for compilers, since they only need to know which symbols exist. The library code itself is responsible for its behavior.

Frama-C, however, in order to perform analyses without having access to the source code of external libraries, requires extra information, typically ACSL function contracts. Extremely simple contracts can be generated automatically (as in, "returns any possible value"), but as soon as there is mutable global state, or pointers being passed to/returned from a function, automatic generation tends to fail.

The usual process of writing a specification consists in:

  1. Reading the English documentation about the function (e.g. its man page, preferably from POSIX, if availale);
  2. Writing requires/assigns/ensures clauses;
  3. Testing and refining the specification to improve how plug-ins handle it.

Even when a function is not in POSIX, there is usually a man page (e.g. from the Linux Programmer's Manual) with an English specification of the function, which may also serve as reference for the ACSL contract.

Due to the sheer amount of existing C libraries, having specifications for all of them is currently infeasible. In order of priority, Frama-C's libc includes specifications from (1) functions in the C standard; (2) POSIX functions; (3) non-POSIX functions (GNU, BSD, etc).

After parsing each source file separately, Frama-C performs a linking step in which function declarations and type definitions are merged if they appear in several files. For instance, if two files both include stdlib.h, there will be two prototypes for malloc(), both referring to the same function. However, two files defining a static function with the same name will lead to two different functions: one of them will be renamed, e.g. with a trailing _1.

During the linking step, if there are multiple ACSL specifications for a given function, they are merged; in particular, if one version of the function has an ACSL specification but not the other, the merged version will have it.

If users want to benefit from Frama-C's libc specifications, they must ensure that (1) FRAMAC_SHARE/libc is included in the preprocessor's include path (this is the default), and (2) an explicit #include directive is present in the code. For instance, a .i source which has been preprocessed while including only standard system headers but not Frama-C's will lack ACSL specifications.

When possible, prefer passing non-preprocessed sources to Frama-C: it is easier to navigate the code, and changes do not require redoing the preprocessing step.

Mixing Frama-C and system headers

A common mistake when using Frama-C consists in mixing headers from Frama-C's libc with those coming from the system, e.g. in /usr/include.

Mixing Frama-C and non-Frama-C headers is error-prone: as a rule of thumb, adding -I/usr/include to -cpp-extra-args only makes sense when using -no-frama-c-stdlib to exclude Frama-C's libc. If unsure, avoid including anything in /usr and try to fix parsing issues as indicated below.

The main reason why mixing headers is discouraged is due to the presence of architecture-specific files in many system headers, namely those in the bits directory. Including a system header may entail recursive inclusion of others, leading to types being redefined in a way that may be incompatible with Frama-C's libc.

Using configure to help parsing

configure scripts can be used to help parsing complex code bases. As an example, let us consider nginx. After downloading its sources and running ./configure, trying to parse most of its files will result in errors such as:

In file included from src/core/ngx_config.h:26:0,
                 from src/core/nginx.c:8:
src/os/unix/ngx_linux_config.h:33:10: fatal error: sys/vfs.h: No such file or directory
 #include <sys/vfs.h>            /* statfs() */

This is because, by default, Frama-C includes its own libc but not the system's. sys/vfs.h is non-POSIX and does not exist in Frama-C's libc.

Short-term solution: copy sys/vfs.h from your system's libc to a directory such as ext_include, then add -I ext_include to -cpp-extra-args. Repeat for each recursively included header, until no more headers remain, or until something breaks. If the latter, remove extraneous definitions in an attempt to remedy the problem.

Long-term solution: see what the real sys/vfs.h file contains, and try to understand if (1) this can be reasonably replicated in Frama-C's libc, or (2) extract only the necessary parts from it and add them to a stubs header. Try to keep portability in mind, using standard types and avoiding compiler-specific features.

Lazy solution: create an empty sys/vfs.h file in a directory that is in the include search path. For instance, create a ext_include directory, then a sys directory inside it, and put an empty vfs.h inside. Add -I ext_include to -cpp-extra-args and try parsing again. This is lazy in the functional programming sense: why try to parse an entire header without knowing if its definitions will actually be necessary? Wait until parsing complains about a missing type or function, and then add those as needed.

WRONG solution: add -I /usr/include to Frama-C's -cpp-extra-args. This may work (or appear to work) in a few cases, but it is likely to lead to complex errors later.

In this specific case, sys/vfs.h is simply a synonym for sys/statfs.h, so we can copy its contents and work on the latter. sys/statfs.h, however, includes bits/statfs.h, which is a red herring: files in bits directories are architecture-specific.

Copying include files from a bits directory is rarely a good idea: their definitions are almost always architecture-specific and clash with Frama-C's portable definitions.

For now, we assume the lazy solution, and try again. This time, we get a missing crypt.h file, which comes from the glibc. Iterating the process, the following files may appear in the list of includes: sys/pctl.h, sys/sendfile.h, sys/epoll.h, linux/capability.h, pcre.h, etc. Most of these are in fact optional and detected when running ./configure. Since ./configure takes into account the underlying system, and not the Frama-C libc, it may detect libraries which we would prefer to have disabled, to avoid having to stub them.

Running ./configure --help, we see several --without-<feature> options, such as --without-pcre, --without-poll_module, etc. Disabling them usually minimizes the amount of external, unspecified code during the analysis.

Most configure scripts allow disabling optional external libraries (e.g. using --without-<feature>); doing so is a good idea to minimize the amount of required stubbing. Alternatively, you can manually edit config.h-style macros such as HAVE_<FEATURE>, setting them to 0.

Importing type definitions

Besides missing includes, the most common case of parsing failure is the absence of type definitions. This is compounded with the fact that error messages about missing types are rarely explicit.

In our nginx example, after setting the missing headers, this is the error message we obtain:

[kernel] src/os/unix/ngx_setaffinity.h:16:
  syntax error:
  Location: line 16, between columns 8 and 18, before or at token: ngx_cpuset_t
  16    typedef cpu_set_t  ngx_cpuset_t;

What the message actually means is that cpu_set_t is unknown. This is because this type is not defined in Frama-C's sched.h, since it is not in POSIX.

Frama-C's libc proritizes definitions in the C standard, and then in POSIX. Other definitions are added when considered useful enough, that is, as soon as a few case studies require them. Until then, they can be easily added to a file such as __fc_stubs.h, to be included as follows:

  1. either by explicitly adding it to the headers requiring it: #include "__fc_stubs.h";

  2. or by using GCC's -include option: -include__fc_stubs.h.

The second option avoids touching the original sources. Also, isolating all such changes in a single file makes it easier to update it when future releases of Frama-C include more definitions, until (hopefully) the file becomes unnecessary.

Finding out which definitions to import

Finding out which definitions to import is not always easy. For instance, in the case of cpu_set_t, first we must find out where it is defined. Using rgrep, ag or similar tools, we just look for the definition in /usr/include. Here, we found it in /usr/include/bits/sched.h:

typedef struct
  __cpu_mask __bits[__CPU_SETSIZE / __NCPUBITS];
} cpu_set_t;

Unfortunately, now we have 3 other definitions to look for: __cpu_mask, __CPU_SETSIZE and __NCPUBITS.

Short-term solution: use gcc -E to preprocess the file and get rid of macros. Note that we cannot do it directly with bits/sched.h, but we can with sched.h, which results in:

typedef struct
  __cpu_mask __bits[1024 / (8 * sizeof (__cpu_mask))];
} cpu_set_t;

Long-term solution: do not preprocess macros away, since they reveal architectural dependencies and other parameters which may be useful later. In our case, __CPU_SETSIZE is actually used elsewhere in nginx, so it is better to preserve it.

In any case, we still have to find out the type of __cpu_mask.

Navigating through type definitions

The layers upon layers of macros and typedefs in the standard library usually require several steps before the actual type definition is found. Using the Frama-C GUI, navigation is often easier.

Short-term solution: use Frama-C and its GUI to quickly get the type: parse the system header file with -frama-c-no-stdlib, then use the Information panel in the GUI to navigate to its definition. Caveat: by default, Frama-C erases unused types, so trying to parse the header itself will result in an empty view in the GUI. Instead, create a very simple test.c file using the target type, as in:

#include <sched.h>

void main() {
    __cpu_mask cm;

Now parse it with frama-c-gui -no-frama-c-stdlib test.c, go to the declaration of m, and use the links in the Information panel to retrieve the type information:

Navigating through types

Important: do not forget to use the proper -machdep when doing this! Type information displayed in the GUI is relative to the chosen machdep. This is one of the reasons to prefer the long-term solution.

This procedure also works with structs and unions, where each field can be queried invididually. However, enum type constants are already unfolded in some cases, so it is not always possible to quickly navigate through them using this method.

Long-term solution: recursively search for each definition in the type, until you get to the bottom of it. This allows a better understanding of typing issues, such as architecture dependencies. In the case of __cpu_mask, we have:

  • typedef __CPU_MASK_TYPE __cpu_mask;
  • then either __UQUAD_TYPE (if on a 64-bit, ILP32 machdep) or __ULONGWORD_TYPE;
  • finally, unsigned long int.

Therefore, a reasonable definition for cpu_set_t might be:

typedef unsigned long __cpu_mask;

# define __NCPUBITS (8 * sizeof (__cpu_mask))
# define CPU_SETSIZE 1024

typedef struct {
  __cpu_mask __bits[CPU_SETSIZE / __NCPUBITS];
} cpu_set_t;

This allows parsing of ngx_setaffinity.h to advance past that point.

Using GCC options to help with parsing failures

Until Frama-C is able to successfully parse the files given in the command line, its AST is incomplete and therefore the GUI cannot be used. In this kind of situation, some GCC-specific options may help with parsing.

The first step usually consists in adding -kernel-msg-key pp to Frama-C's command line. This will output the preprocessing command Frama-C uses when parsing each file, similar to this:

  preprocessing with "gcc -E -C -I.  -I~/.opam/4.02.3/share/frama-c/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc -m32 file.c"

It is then easy to copy/paste the command in the terminal to modify it, adding/removing flags. For instance, using GCC's -M flag, the list of files included during preprocessing is displayed as a Makefile rule. This makes it easier to identify e.g. if files from different C standard libraries were mixed together.


There are several techniques to help Frama-C parse realistic code bases, some consisting of "quick fixes", others requiring more effort but providing long-term benefits in terms of stability and portability. Further changes are required according to the plug-ins to be used (e.g. function contracts for WP and Eva), but since parsing is the first step required by all plug-ins, preparing a working set is an effort that can be easily factored for other users to benefit from. This is one of the objectives of the open-source-case-studies Github repository: sharing such a configuration so that users only need to type make parse to get a ready-to-use AST, to be loaded and used with any plug-in they desire. Do not hesitate to contribute to it, either requesting or offering such parsing configurations.

Tuesday, June 19 2018

Analyzing Chrony with Frama-C/Eva

Chrony is an implementation of NTP which is C99-compatible, with portable code, and thus a good candidate for an analysis with tools such as Frama-C.

As part of an effort sponsored by Orolia, researchers from the List, CEA Tech laboratory applied Frama-C/Eva on the Chrony source code, in an attempt to verify the absence of run-time errors. This post summarizes some of the findings and links to the full report, in PDF format.

Scope of the analysis

The analysis was performed on Chrony 3.2.

Some parts of the code were disabled via the configure scripts, namely IPV6, timestamping and readline. The idea is to minimize the amount of non-POSIX code, in hopes of improving the likelihood that external functions will have a specification in Frama-C's stdlib. Reenabling those features requires only writing additional stubs/specifications.

The entrypoint used for the analysis was the main function in test/unit/ntp_core.c, with a generalized state for argc and argv, to include possible behaviors from arbitrary command line arguments.

The Eva plug-in was iteratively parametrized to improve coverage and minimize the number of alarms, while maintaining a short execution time. Reported alarms include possible buffer overflows, uninitialized reads, and other undefined behaviors, as listed in the Eva plug-in user manual.

The analysis identified a few issues, but the overall impression was that code quality was high w.r.t. the C standard and the presence of some defensive programming patterns. However, there are still several potential alarms that need to be further investigated to ensure the absence of run-time errors.

The full report is available here:

Report: Frama-C/Eva applied to the Chrony source code: a first analysis (PDF)

Do not hesitate to contact us if you have suggestions, remarks, patches, etc. You can use the Frama-C mailing list or Github's issues page on open-source-case-studies.

Thursday, February 15 2018

Analysis scripts: helping automate case studies, part 2

In the previous post, we used analysis-scripts to prepare our analysis of Recommender. In this post, we will run EVA on the code and see how the iterative refinement of the analysis can be done. We assume the reader has performed all of the steps in the previous post, and is currently in the directory containing the GNUmakefile created previously.

Running the first EVA analysis

Running make main.eva will run the EVA plug-in in the console, and then output some metrics information. This is useful for scripts and experienced users. For now, running make main.eva.gui is more useful: it will run the analysis and then open the results in the GUI.

A *.{parse,eva}.gui target in analysis-scripts only run parsing/EVA if necessary; if it has already been run, and no source files or analysis parameters were modified, it will directly open the GUI.

In the GUI, in the Properties panel (you have to click Refresh after loading the GUI) if we inspect only Unknown/Invalid properties, we will notice 148 of them, several related to finiteness of floating-point values, as well as many related to variable initialization.

Note that the results of each analysis are stored in the main.eva directory, and also copied to a timestamped directory in the form main_YYYY-MM-DD_hh-mm-ss.eva. Thus main.eva always contains the latest analysis, while the timestamped copies are useful to retrieve past results and compare them, e.g. using meld's folder comparison view.

Iterating on EVA analyses

Let us use the Loop Analysis plug-in to obtain more precise results. Since analysis-scripts already created a Frama-C save file (extension .sav by default), we just need to load it and add -loop:

frama-c -load main.eva/framac.sav -loop > main.slevel

Open the main.slevel file with a text editor. It contains the output of the Loop Analysis plug-in: some informative text, and then a line that says:

[loop] Add this to your command line:

Followed by several command-line arguments related to the use of slevel. Let us erase everything up to and including the Add this ... line, and then include the file contents in the EVAFLAGS variable of our GNUmakefile:

EVAFLAGS    += $(shell cat main.slevel | tr '\\' ' ')

Note that we use the tr command-line utility to remove the backslashes from the output of Loop Analysis.

If we re-run make main.eva.gui, the dependencies managed by Make will re-run the analysis because its command-line changed, but not the parsing, since it was not impacted.

This time, we obtain 114 unknown/invalid properties.

Appeal to brute-force

Since this is a test case that runs very quickly, and because Loop Analysis' heuristics are not perfect, we can allow ourselves to try a somewhat aggressive -slevel. Let us remove the heuristics given by Loop Analysis, and instead use a global slevel of 500:

EVAFLAGS    += -slevel 500

The reason why we remove Loop Analysis' results is that, in some cases, it forces merging of states to avoid slowing down the analysis, and those settings take precedence over the global slevel.

The analysis will be much longer this time, but should still terminate in a few seconds. Given such a high slevel, we are lucky that it terminates at all. We will obtain 86 unknown/invalid properties this time.

Extra hypotheses for more precision

There are several options in EVA that allow a more precise analysis of less-than-ideal code that can be found in the wild. Most of them require knowing some details about the semantics of C, but others can be used more leniently, to help get a better idea of the code under analysis, before some serious analysis time is spent. One of them is -no-val-malloc-returns-null. This option is only useful when the code contains dynamic memory allocation, and what it does is to consider that memory allocation never fails.

By default, the memory allocation built-ins used by EVA suppose that memory allocation can fail, as stated in the standard (i.e. malloc can return NULL, for instance when there is not enough available memory). However, many code bases fail to test for such cases; which is admittedly a relatively rare situation, especially on a system that allows memory overcommitment. The -no-val-malloc-returns-null thus adds a new hypothesis to the underlying analysis ("... and considering that memory allocation never fails..."), in exchange for a more precise result.

In Recommender, we notice that there are some spots where malloc is tested for NULL (e.g. in src/learned_factors.c:47), but others where no such test is performed (e.g. in src/learned_factors.c:67). Thus adding this option should (hopefully) result in fewer alarms. Our EVAFLAGS line becomes:

EVAFLAGS    += -slevel 500 -no-val-malloc-returns-null

Indeed, running the analysis again results in only 56 unproved properties. However, it also reveals another issue.

Tracking red alarms

Opening in the GUI the result of the last iteration of the analysis, if we scroll through the main function, we see that the analysis has stopped (became red) before returning from the call to recommend_items. Jumping to its definition, we see a loop where j should go from 0 to 2 (the value contained in (estim_param->tset)->items_number)), but inspecting the value of j in the while condition shows {0; 1}. This means that the third iteration never took place, its trace cut short by some evaluation that resulted in a definitely invalid property.

There are several ways to proceed here:

  • One can follow the "red path" in the GUI, jumping inside reachable functions in the GUI until the limit of the red path is found;

  • Alternatively, in this case we have a warning (in the Messages tab) that says that all target addresses were invalid, which often indicates an issue with the evaluation of a state;

  • Finally, one can prioritize alarms in the Properties tab, by checking only Invalid properties at first, before including Unknown ones.

In this case, all three would end up around the same source line (src/binary_heap.c:153), though this is not always true.

Spoiler alert: the Chlorine 17 release of Frama-C will include an extra panel, Red alarms, which will provide another way to get to properties that warrant extra attention when starting an analysis.

Note that, whenever the C code contains calls to assert(), Frama-C generates a call to __FC_assert whose precondition is requires \false. This leads to an Invalid alarm in the Properties panel, however this does not indicate that the source code necessarily has undefined behavior: it may be due to an imprecision in the assertion condition, which if possibly true, leads to the call being made, which will itself definitely indicate an error. But if the call may not happen, then the assertion should be treated like an Unknown alarm.

Spoiler alert: in Frama-C Chlorine (17), the behavior of assert will be changed to more closely match the usual approach: an Invalid alarm will only be generated when the assertion is definitely violated.

Back to the Invalid alarm: if we inspect the source code in question, we will see that the only valid index for the buffer bheap->buffer is 0, due to the ACSL assertion inserted by EVA:

/*@ assert Value: index_bound: bheap->filled_elements < 1; */
bheap->buffer[bheap->filled_elements] = value;

However, filled_elements is 1 in this call, which seems like an error. But why is it there? While it is impossible to know exactly the intent of the author of the code, by inspecting the definition of the buffer, we can obtain some clues. In the Information panel, if we inspect bheap, we see that:

Variable bheap has type `binary_heap_t *'.
It is a formal parameter.
It is referenced and its address is not taken.

And then if we click binary_heap_t itself, we obtain its type information:

Type information for `binary_heap_t':
(sizeof 16, defined at src/binary_heap.h:53)
 struct binary_heap {
    size_t max_size ;
    size_t filled_elements ;
    int (*value_comparer)(void const *, void const *) ;
    void *buffer[1] ;

Finally, clicking the source line will take us to the definition in the binary_heap.h header, which contains some useful comments:

 * binary_heap:  The heap is tree based data structure
 * Members:
 *   max_size        The number of elements in the binary heap
 *   filled_elements The number of inserted elements so far
 *   buffer          The buffer is a dynamically allocated array
 *                   containing the heap's elements
typedef struct binary_heap
  size_t          max_size;
  size_t          filled_elements;
  bh_value_cmp    value_comparer;
  void*           buffer[1];
} binary_heap_t;

From the comment, it seems that the code is implementing the pattern of a flexible array member, where the last element of the binary_heap_t structure should be an incomplete array type. However, its current declaration corresponds to that of a fixed-size array, which according to the C standard cannot be accessed beyond its static bounds. We can fix this by using the proper flexible array member notation defined in the C99 standard.

Syntactic fixes

By replacing void* buffer[1]; with void* buffer[]; in src/binary_heap.h, we define a proper flexible array member. As a consequence, the code can access all elements of the dynamically-allocated array, as long as enough memory has been allocated for them.

You may notice that, after modifying the .h file and re-running make main.eva.gui, Make will not re-parse nor re-run the analysis, it will simply open the GUI again. This is because the .h file dependencies are not tracked by the Makefile rules: they were never included in the list of .c sources of main.parse (because such headers are directly included via preprocessor directives), so Make has no way to know about these implicit dependencies. You can remedy that by forcing Make to unconditionally make all targets, adding -B to the command line arguments.

After doing so, everything is recomputed, and we obtain … almost the same alarm.

This time, the alarm happens on the third iteration of the loop, instead of the second one: progress! … But not much. There is still a problem when accessing the last element of the array. To find out why, we can use the GUI again. However, this time the Invalid alarm is no longer present; the problem is more subtle. Still, the warning about all target addresses were invalid is still there. It points to this statement:

    /*@ assert
        Value: mem_access: \valid(&bheap->buffer[bheap->filled_elements]);
    bheap->buffer[bheap->filled_elements] = value;

By inspecting bheap->filled_elements, we see its possible values were {1; 2} before the statement, but {1} afterwards. This indicates that index 2 is not valid for this memory access. But why? We can check the location being accessed, to see its validity.

If we inspect the values for bheap, we see, in the Values tab:

bheap -> {{ (binary_heap_t *)&__malloc_init_binary_heap_l42 }}

Then, if we left-click on __malloc_init_binary_heap_l42, the Information panel will display some extra lines about this value in particular, with a clickable link pointing to its syntactic information. Clicking on that link will display the type of the dynamically allocated block:

Variable __malloc_init_binary_heap_l42 has type `char [23]'.

For dynamically allocated bases, EVA does not always have access to the original type intended for the allocated base, so it uses heuristics to restore that information. When such heuristics fail, it resorts to the "catch-all" char [].

"23" is a somewhat unusual size (not a multiple of the word size). Let us investigate where that number came from.

Using Studia

Right-clicking on __malloc_init_binary_heap_l42, in the Information tab, will display a context menu, the same one as if we had right-clicked some lvalue on the Cil code. We will use the Studia plug-in, in particular its Writes feature, to identify all points in the source code where this memory location was written prior to the statement indicated by the warning.

Studia will compute and highlight the statements in the code, and also add an extra column to the filetree display (upper left corner in the GUI), indicating all functions directly writing to the memory location (indicated by a 'tick' symbol in the Studia column) and the functions indirectly writing to it, that is, the callers of the former (indicated by an arrow symbol in the Studia column) as well as their own callers, recursively.

The functions writing to buffer are: balance_heap, init_binary_heap and insert_binary_heap. The first and the last write to fields in the buffer structure, but only init_binary_heap actually allocated the memory.

Well, I guess you could have directly inferred that from the variable name, which serves this exact purpose, but then I wouldn't have had an excuse to shamelessly plug Studia, one of the new features in Frama-C 16 Sulfur, would I?

Inside init_binary_heap lies our answer: the computation of the size of the bheap includes a -1, which is due to the fact that the non-flexible array member notation already had a byte allocated for the array, but our proper C99-compatible version no longer includes this byte. So the malloc'ed memory was 1 byte shorter, which led to the invalid memory access. So all we have to do is to fix the computation here (and take note of the fact that modifying other people's code without properly understanding it can lead to bugs).

At last … unable to progress

This time, we re-run the analysis (no need to use -B this time, since the .c file is tracked in the dependencies of our GNUmakefile), expecting to triumph over the syntactic distractions. However, we are greeted with a somewhat unpleasant surprise:

src/binary_heap.c:118:[value] warning: detected recursive call
    (balance_children <- balance_children :: src/binary_heap.c:135 <-
                         pop_binary_heap :: src/recommender.c:95 <-
                         recommend_items :: test/test.c:108 <-
    Use -val-ignore-recursive-calls to ignore (beware this will make the analysis
[value] user error: Degeneration occurred:
    results are not correct for lines of code that can be reached from the degeneration point.

We should have seen it coming: binary heaps are fond of recursion. Our coverage did improve from the previous analysis (from about 75% to about 85%), but we now hit a harder obstacle. To deal with this, we'll have to stub the balance_children function, possibly over-approximating its behavior, or rewrite an equivalent, iterative version of the function. In either case, such transformations are out of the scope of this tutorial.

Conclusion and bonus features

In this tutorial, we showed how to use analysis-scripts, presenting most of its features in a quick usage scenario. There are still a few tricks up its sleeve which were not mentioned:

  • flamegraph.txt: this file is computed by option -val-flamegraph, and it produces a Flamegraph of the analysis performed by EVA. This graph is useful when profiling larger case studies, to quickly visualize where the analysis is spending most of its time. This can indicate functions where less slevel or ACSL stubs might help.

  • metrics.log: its output is displayed after running a .eva target. The coverage estimation is a quick indicator of progression in the analysis during the refining stage, i.e. sometimes when an analysis is made more precise, the number of alarms may actually increase, and the reason may be that the coverage has improved, so that more code is actually being analyzed, which might explain why now there are more alarms.

  • alarms.csv: a CSV report with the same contents of the Properties panel in the GUI, obtained via the Report plug-in. Very useful for scripts.

  • stats.txt: similar to the one present in the .parse directory; however, since parsing is usually very fast when compared to an EVA analysis, this version of the file is the one that is actually useful most of the time. In particular, if you want to compare the execution time of a new parameterization of the analysis, you just need to look at the user_time line. Very useful when you realize you forgot to type time make instead of make.

We hope this tutorial was useful to you and that the next Frama-C release will make things even easier! Don't forget to check some usage examples in open-source-case-studies, and please consider proposing your own case studies via Github issues.

Thursday, January 25 2018

Analysis scripts: helping automate case studies, part 1

(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.

This series supposes some familiarity with EVA, as in, its basic usage is not detailed. Reading A simple EVA tutorial or the tutorial in the EVA user manual should be sufficient.

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.

Analysis scripts

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 ( which contains the bulk of it.

Note: the mentions 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

To illustrate the use of analysis-scripts, we picked one project from ffaraz's awesome-cpp repository: GHamrouni's Recommender, a library from the Machine Learning section.

We start by cloning the repository1:

git clone

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 649fbfc in 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 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 compile_commands.json

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 -W and -O), but it also contains preprocessor flags, mostly -I and -D, which we are interested in.

The compile_commands.json file can be produced as follows:

  1. If the project is based on CMake, add -DCMAKE_EXPORT_COMPILE_COMMANDS=ON to the cmake command-line, e.g. instead of cmake <source dir>, use cmake <source dir> -DCMAKE_EXPORT_COMPILE_COMMANDS=ON.

  2. If the project is based on Makefile, use Build EAR. After Build EAR is installed, you just have to prefix make with bear: typing bear make is usually enough to obtain the JSON database.

Note: Frama-C 17 (Chlorine) includes option -json-compilation-database, which allows using compile_commands.json directly, rendering the next step unnecessary.

Once you have the file, simply grep it for -I and -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), CPPFLAGS.

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:

  1. GNU Make gives preference to GNUmakefile over Makefile if both exist, so the default file used when typing make will be ours, even if the project already has its own Makefile;

  2. This avoids having to rename/overwrite existing makefiles (or, worse, having Frama-C's Makefile erased when re-running ./configure);

  3. The analysis-scripts Makefile 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.

Our 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 PATH to keep the template concise.

include $(shell frama-c-config -print-share-path)/analysis-scripts/

# Global parameters
FCFLAGS     +=


# 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 .parse and .eva, which are hard-coded in the analysis-scripts' Makefile to generate targets with the appropriate dependencies and rules.

The .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 make, since 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 main function.

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:

make main.parse

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 CPPFLAGS:


Running 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 (CPPFLAGS or FCFLAGS), Frama-C will not waste time reparsing the results: they have already been saved inside the main.parse directory.

Contents of the .parse directory

For each .parse target, 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 warnings.log).

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.sav can be used with frama-c -load, for instance when trying different plug-ins;

  • parse.log contains 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.

Thursday, September 21 2017

Frama-C appears on European Commission's Innovation Radar


Frama-C is among the 10 innovative products selected in the "Tech for society" category. Be sure to cast your vote to help your favorite static analyzer making its way through the final in Budapest.

Stance Project

Between 2012 and 2016, CEA Tech List was the coordinator of the STANCE project, funded by the European Union under the 7th Framework Programme (FP7). The main goal of STANCE was to show how formal verification tools, including of course Frama-C, could be used for assessing security properties in sensitive programs.

Among many other results, the project has seen the development of various Frama-C plug-ins by CEA Tech List, including Frama-Clang, E-ACSL, EVA, WP, Slicing and From. Other partners (Dassault Aviation, Thales, Technical University of Graz, and Infineon) did use Frama-C over their own, and wrote themselves a certain number of plug-ins to help their analyses, while Search Labs provided a plug-in to combine Frama-C with their own fuzz testing tool, Flinder, in order to generate test cases triggering an alarm emitted by Value Analysis. Finally, Trusted Labs evaluated the benefits brought by Frama-C in the context of a Common Criteria security evaluation.

EC's Innovation Radar

All in all, it seems that the project was evaluated very positively by the European Commission, which has just selected Frama-C among the 10 best innovators in the Tech for Society category. We would like to thank all the participants to the STANCE project for this great achievement, and we hope that is a good omen for STANCE's successor, VESSEDIA, which gather many partners already present in STANCE and is more directed towards safety and security in industrial control systems.

Call to the Public

Now, our presence in this list is not the end. Indeed, a public vote will now select 4 finalists who will defend their project in November in Budapest, where a jury will choose the winner. If you think that cybersecurity is important and formal methods such as advocated by Frama-C should play a major role in it, don't hesitate to cast your vote (and share the link in all social networks you're connected to, of course). In the mean time, if you have project ideas in which Frama-C could fit, we would of course be glad to hear from you.

Tuesday, June 13 2017

Frama-C 15 (Phosphorus) released, and open source case studies

Frama-C 15 (Phosphorus) has been released, and the OPAM package is already available! A MinGW-based OPAM package, distributed by fdopen's MinGW OPAM repository, is also available.

In this post, we briefly highlight two new features in this release. We also announce the release of a new Github repository, open-source-case-studies, which contains some snapshots of code bases ready to be analyzed with Frama-C/EVA.

Highlighted new features

E-ACSL in the default release

One notable change in this release is the direct integration of E-ACSL: instead of having to install OPAM packages frama-c and frama-c-e-acsl, you only need to install frama-c.

E-ACSL enables runtime verification in Frama-C, serving as an efficient tool for detecting undefined behavior and for debugging ACSL specifications. It can be used in a "stand-alone" mode (e.g. with assertions generated by the RTEgen plug-in), or in combination with EVA, in which case its instrumentation is more efficient: EVA only generates ACSL assertions for the properties that it cannot prove, thus greatly reducing E-ACSL's instrumentation.

Note that, due to the usage of jemalloc and some technical details, E-ACSL is disabled by default in Mac and Windows.

Better pretty-printing of #include directives

One of the drawbacks of the -print option of Frama-C was the fact that the code was entirely preprocessed, expanding a Hello world example to several hundreds of lines, due to the expansion of #include <stdio.h> and derived files.

There are now two options, -print-libc and -no-print-libc (the latter is enabled by default) which control the folding/unfolding of #include directives in pretty-printed code. More specifically, if your original code is:

#include <stdio.h>

int main() {
    printf("hello world!\n");
    return 0;

Then the result of -print will be:

/* Generated by Frama-C */
#include "errno.h"
#include "stdarg.h"
#include "stddef.h"
#include "stdio.h"
/*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
int printf_va_1(char const *format);

int main(void)
  int __retres;
  printf_va_1("hello world!\n");
  __retres = 0;
  return __retres;

There are two interesting things to notice here:

  1. Some #include directives are present at the beginning of the file. These directives correspond to all files from the Frama-C standard library whose identifiers were present in the (expanded) original code. For instance, errno.h is present because Frama-C's stdio.h includes it. As you can see, the mechanism does not guarantee a minimal number of includes, but it is much cleaner than having all files expanded;

  2. The specification of printf_va_1 is visible. This is due to the fact that the Variadic plug-in (which is enabled by default on Frama-C 15 (Phosphorus)) generated this specification - it is not part of the standard Frama-C library. In fact, printf_va_1 is a specific instantiation of the variadic printf function. You can disable the automatic variadic translation with -variadic-no-translation, in which case -print will result in:

/* Generated by Frama-C */
#include "errno.h"
#include "stdarg.h"
#include "stddef.h"
#include "stdio.h"
int main(void)
  int __retres;
  printf("hello world!\n");
  __retres = 0;
  return __retres;

The Phosphorus release also includes, as usual, a series of bug fixes and minor improvements. Consult the Changelog for more details.

Open source case studies

A new Github repository on the Frama-C organization, open-source-case-studies, has been created to help users quickly run Frama-C (and EVA in particular) in more realistic code bases, which includes different sorts of open-source code; some of them are very small (a single file) while others contain significantly larger bases. Their usage is very simple: once you have installed Frama-C and put it in the PATH, enter one of the case study directories and run:

  • make to parse and run EVA;

  • make <target>.eva.gui to open the Frama-C GUI and view the results.

The target names vary on each case study, and can be obtained via make help. Note that this will show only the base target name, from which other targets are derived (e.g. <target>.parse, <target>.eva, <target>.eva.gui).

All case studies include a Makefile, which uses the files in fcscripts to generate targets and Makefile rules to allow running EVA quickly. Among the facilities provided by these scripts, we highlight:

  • templates for Frama-C parametrization (i.e. variables CPPFLAGS, FCFLAGS and EVAFLAGS to delineate which options are related to preprocessing, parsing and running EVA), including helpful default parameters;

  • automatic target dependencies on command line arguments: Frama-C reparses files only when they are modified, and re-runs EVA only when command line arguments change;

  • saving of intermediate results in directories (for easy comparison via Meld), to run other plug-ins without having to re-run EVA (e.g. frama-c -load <target>.eva/framac.sav ...).

Note, however, that there are some caveats concerning this repository:

  1. It is not representative of the scale of programs that Frama-C/EVA can handle; indeed, all large code bases where Frama-C/EVA is applied consist in industrial code that cannot be shared;

  2. One of the main purposes of the repository (internally) is to serve for non-regression testing, which means that some analyses are not fully parametrized;

  3. Some case studies include code that is not ideally dealt with by EVA, but may be useful for other plug-ins.

Those caveats aside, we hope this repository will give practical examples and help you to parametrize your own analyses. If you also have some interesting open source code bases on which to run EVA, you can submit them to us as a Github pull requests. This will make it easier to compare the behavior of future versions of Frama-C on such code, and to benefit from improvements in the analyzer.

Tuesday, April 11 2017

A simple Eva tutorial, part 3

On the previous post we've seen how to run Eva, but at the end we had a NON TERMINATING FUNCTION for a function that is supposed to always terminate, a likely indication that a definitive undefined behavior has been found in the analysis. In this post, we will see how to diagnose such cases, using derived plug-ins and the GUI.

We will reuse the save file produced at the end of the analysis, value2.sav.

When the GUI is not enough

Usually, after running the value analysis in the command-line, we launch the GUI to visualize the results:

frama-c-gui -load value2.sav

In this case, because of the NON TERMINATING FUNCTION message, we know that at some point in the program we will have red statements in the GUI, which indicate unreachable code.

By scrolling down from the main function, we reach the non-terminating statement, which is a call to test_x25519:

Unreachable code in the Frama-C GUI

Note the red semicolon at the end of the statement, and the fact that the following statements are also red. If we click on the statement, the Information panel says that This call never terminates.

You can right-click on the function and Go to the definition of test_x25519, and you will find the same thing inside, this time a call to crypto_x25519_public_key, and so on, until you reach fe_tobytes, which is slightly different: it contains a for loop (defined via a macro FOR), after which all statements are red, but the loop itself is not an infinite loop: it simply iterates i from 0 to 5. How can this be non-terminating?

The answer, albeit non-intuitive, is simple: there is one statement inside the loop which is non-terminating, but not during the first iteration of the loop. Because the GUI colors are related to the consolidated result of all callstacks (i.e., if there is at least one path which reaches a statement, it is marked as reachable), it cannot show precisely which callstack led to the non-termination. To better understand what happens here, we will use the Nonterm plug-in.

Nonterm to the rescue

Nonterm is a small plug-in that uses the result of the value analysis to display callstack-wise information about non-terminating statements, by emitting warnings when such statements are found. It requires Eva to have been executed previously, but it runs very quickly itself, so you do not need to save its results. Close the GUI and re-run it again, this time with Nonterm:

frama-c-gui -load value2.sav -then -nonterm -nonterm-ignore exit

The -nonterm-ignore exit argument serves to minimize the number of warnings related to calls to the libc exit() function, which is always non-terminating.

The warnings generated by Nonterm are displayed in the Messages panel, after those emitted by Eva.

Examples of Nonterm warnings

The warnings display the non-terminating callstacks. The order of the warnings themselves is not relevant. However, some kinds of warnings are more useful than others. Here is a rough indication of their relevance, from most to least precise:

  1. Non-terminating statements;
  2. Non-terminating loops;
  3. Non-terminating function calls;
  4. Unreachable returns.

In our analysis, the first (and only) warning about a non-terminating statement is the following:

Non-terminating statement

Note a few important details about the Frama-C GUI:

  • When you click on the warning in the Messages panel, the GUI focuses on the related statement.
  • When a statement has associated annotations (here, two warnings), the focus is placed on the first annotation, instead of the statement itself. This does not imply that the annotation itself is related to this specific warning.
  • The property status indicators (colored circles, or bullets on the left of each property) display the consolidated status of all callstacks; in particular, if the property is definitively valid in one callstack, but possibly/definitively invalid in another, the GUI displays a yellow bullet.

Nonterm restores some of the information lost due to callstack consolidation. The highlighted warning in particular gives us the following information:

  1. There exists a stack trace in which statement h5 -= c5 << 25 does not terminate;
  2. There is exactly one stack trace in which the statement never terminates; all other stack traces (which are not shown in the warning) terminate.

Currently, it is not possible to select a stack trace from the Messages panel, but we can do so using the Values panel. If we switch to it (keeping the statement highlighted in the source code), we can see that there are 40 different stack traces reaching this point.

Values Panel

The Values panel is arguably the most powerful inspection tool for the Eva plug-in in the Frama-C GUI. Some of its features were presented in earlier posts, but for the sake of completeness, here are some commented screenshots:

Values panel

The values displayed in this panel are related to the green highlighted zone in the Cil source.

The Ctrl+E shortcut is equivalent to highlighting a statement, then right-clicking Evaluate ACSL term. The Ctrl+Shift+E shortcut is slightly more powerful: it also evaluates terms, such as \valid(p). This command is not available from any menus.

The Multiple selections checkbox allows adding several expressions to be compared side-by-side. When checked, highlighting an expression in the same statement adds a column with its value. Note that highlighting a different statement results in resetting all columns.

The three checkboxes to the right are seldom used: Expand rows simply expands all callstacks (but generates visual clutter); Consolidated value displays the row all (union of all callstacks); and Per callstack displays a row for each separate callstack.

The callstacks display has several contextual menus that can be accessed via right-clicks.

Callstacks display

Let us start from the bottom: right-clicking on a callstack shows a popup menu that allows you to focus on a given callstack. This focus modifies the display in the Cil code viewer: reachability will only be displayed for the focused callstack(s). We will come back to that later.

Right-clicking on a cell containing a value allows filtering on all callstacks for which the expression has the same value. This is often used, for instance, to focus on all callstacks in which a predicate evaluates to invalid or unknown.

Finally, clicking on the column headers allows filtering columns.

Note that the Callstacks column header displays a pipette icon when a filter is being applied, to remind you that other callstacks exist.

Filtering non-terminating callstacks

In our code, despite the existence of 40 callstacks, only one of them is non-terminating. If you highlight the 0 ≤ c5 expression before statement h5 -= c5 << 25, you will see that only a single callstack displays invalid in the column 0 ≤ c5. Focus on this callstack using the popup menu, then highlight expression c5 in the Cil code. You will obtain the following:

Focused on a non-terminating callstack

As you can see, the GUI now displays the statements following h5 -= c5 << 25 in red, indicating thay they are unreachable in the currently focused callstacks. The exact value that caused this is shown in column c5: -1. The C standard considers the left-shift of a negative number as undefined behavior. Because -1 is the only possible value in this callstack, the reduction caused by the alarm leads to a post-state that is <BOTTOM>.

Proceeding with the analysis

To allow Eva to continue the analysis of the code, we need to modify it in some way. Since we are not experts in cryptography, we are unable to provide a definitive explanation why the code was written this way. In any case, it is not specific to Monocypher, but also present in TweetNaCl and ref10, two cryptographic libraries.

It is likely that replacing the signed carry variables in function fe_mul with unsigned ones would get rid of the undefined behavior, without changing the expected behavior of the code. However, without a more formal analysis performed by a cryptographer, this is just guesswork. Still, we need to do something to be able to continue the analysis (and possibly spot more undefined behaviors), such as changing the declarations of variables c0 to c9 to u64 instead of i64. Then, re-parse the sources, re-run the analysis, and keep iterating.

Ideas for complex situations

In the beta version of this post, we were using version 0.1 of Monocypher, which had a different version of functions related to fe_mul. In particular, some of the functions were taken from TweetNaCl, and the code was not unrolled the same way as in Monocypher 0.3. One of the consequences was that Nonterm was unable to show as clear a picture as in this case; it was necessary to perform syntactic loop unrolling (e.g., using loop pragma UNROLL) just to be able to clearly see in the GUI which statement was non-terminating.

Future developments in Frama-C and in the Eva plug-in will help identifying and visualizing such situations more easily.


We would like to thank loup-vaillant (Monocypher's author) for the discussions concerning Monocypher and Eva's analysis. New versions of Monocypher have been released since the analysis performed for this series of posts, which do not present the undefined behavior described in this post.

Friday, March 17 2017

A simple Eva tutorial, part 2

On the previous post we've seen some recommendations about using Frama-C/Eva, and some tips about parsing. In this post, we will see how to run Eva, and how to quickly setup it for a more precise result.

We will reuse the save file produced at the end of the parsing, parsed.sav.

First run of Eva

The default parameters of Eva are intended for a fast analysis. In Frama-C 14 (Silicon), option -val-builtins-auto is recommended to enable the usage of built-in functions that improve the precision and sometimes the speed of the analysis1.

1 This option will be enabled by default in Frama-C 15 (Phosphorus).

The following command-line should result in a relatively quick first analysis:

frama-c -load parsed.sav -val-builtins-auto -val -save value.sav

Note that we save the result in another file. It can be reused as input for another analysis, or visualization in the GUI.

The analysis will likely output many alarms, some due to loss of precision, others due to an incorrect setup. Here are a few important alarms concerning an incorrect setup:

  1. Missing code or specification

    file.c:42:[kernel] warning: Neither code nor specification for function foo, generating default assigns from the prototype

    There are two major causes for this warning: (1) the file containing the function definition was not given to Frama-C during parsing; or (2) the function has no source code and no ACSL specification was given.

    In the first case, the solution is to include the missing source file. Parsing will succeed even if only a declaration (function prototype) is present, but Eva requires more than that. It may be necessary to return to the parsing stage when this arrives.

    In the second case, you must supply an ACSL specification for the function, otherwise Eva will assume it has no effect, which may be unsound. To do it with minimal modifications to the original code, you can do the following:

    1. create a file, say stubs.h;
    2. copy the function prototype to be stubbed in stubs.h (adding the necessary #includes for the types used in the prototype);
    3. add an ACSL specification to this prototype;
    4. include stubs.h in the original source, either by adding #include "stubs.h", or using GCC's -include option (e.g. -cpp-extra-args="-includestubs.h", without spaces between -include and the file name).
  2. Missing assigns clause, or missing \from

    When analyzing functions without source code, Eva imposes some constraints on the ACSL specification: they must contain assigns clauses, and these clauses must have \from dependencies. Otherwise, warnings such as the following may be generated:

    foo.c:1:[value] warning: no 'assigns \result \from ...' clause specified for function foo
    foo.c:3:[value] warning: no \from part for clause 'assigns *out;' of function foo
    foo.c:6:[kernel] warning: No code nor implicit assigns clause for function foo, generating default assigns from the prototype

    The following is an example of an incomplete specification:

    /*@ assigns *out; */
    void foo(int in, int *out);

    Even if it contains an \assigns clause for pointer out, it does not say where the result comes from. Adding \from in, for instance, makes the specification complete from the point of view of Eva.

    Note: Eva cannot verify the correctness of the specification in the absence of code, especially that of ensures clauses. If you provide an incorrect specification, the result may be unsound. For that reason, it is often useful to write a simplified (or abstract) implementation of the function and then run the analysis. If Eva has both the code and the specification, it is able to check ensures clauses and detect some kinds of errors.

Running Eva on monocypher

Running Eva on parsed.sav will start the value analysis on the main function defined in test.c. Due to the large number of small functions in Monocypher, Eva will output a huge amount of lines, whenever a new function is entered. Adding option -no-val-show-progress will omit messages emitted whenever entering a new function.

Also, the fact that this code contains lots of small functions with few or no side-effects is a very strong indicator that -memexec-all will be very helpful in the analysis.

Memexec, which is part of Eva, acts as a cache that allows reusing the result of function calls when their memory footprint is unchanged. It dramatically improves performance.

Combining both options, we obtain the following command-line:

frama-c -load parsed.sav -val -val-builtins-auto \
        -no-val-show-progress -memexec-all -save value.sav

The analysis will then start and emit several warnings (mainly due to imprecisions). It should finish in a few seconds, depending on your processor speed.

Improving Eva results

After running the value analysis, it is a good time to check what the result looks like, using the GUI:

frama-c-gui -load value.sav

In the screenshot below, we indicate some parts of the GUI that are useful when inspecting Eva results (besides the source view). We also indicate some parts that are never (or rarely) used with Eva.

Frama-C GUI for Eva

Note that the Properties tab (between Console and Values) is not updated automatically: you need to click on the Refresh button before it outputs anything, and after changing filters.

Several tips concerning this panel were presented in a previous post about the GUI. If you follow them, you will be able to make the Properties panel show the total of Unknown (unproven) properties for the entire program, and only those. This number is often similar to the number of messages in the Messages panel.

In Monocypher, after setting the filters to show every Unknown property in the entire program, and clicking Refresh, we obtain over 900 unproven properties. Since the analysis was not tuned at all for precision (other than with -val-builtins-auto), this number is not particularly surprising.

A quick way to improve on results is to use the Loop analysis plug-in.

The Loop analysis plug-in performs a mostly syntactic analysis to estimate loop bounds in the program (using heuristics, without any soundness guarantees) and outputs a list of options to be added to the value analysis. Running Eva again with these options should improve the precision, although it may increase analysis time. Loop analysis' main objective is to speed up the repetitive task of finding loop bounds and providing them as semantic unrolling (-slevel) counters. The analysis may miss some loops, and the estimated bounds may be larger or smaller, but overall it minimizes the amount of manual work required.

Loop analysis does not depend on Eva, but if it has been run, the results may be more precise. In Monocypher, both commands below give an equivalent result (the difference is not significative in this context):

frama-c -load parsed.sav -loop
frama-c -load value.sav -loop

In both cases, Loop analysis' effect is simply to produce a text output that should be fed into Eva for a new analysis:

[loop] Add this to your command line:
       -val-slevel-merge-after-loop crypto_argon2i \
       -val-slevel-merge-after-loop crypto_blake2b_final \

You should, by now, use a shell script or a Makefile to run the Frama-C command line, adding all the -val-slevel-merge-after-loop and -slevel-function lines to your command.

Let us consider that the environment variable LOOPFLAGS contains the result of Loop analysis, and EVAFLAGS contains the flags mentioned previously (-no-val-show-progress, -val-builtins-auto and -memexec-all). Then the following command will re-run Eva with a more detailed (and, hopefully, precise) set of parameters:

frama-c -load parsed.sav $LOOPFLAGS -val $EVAFLAGS -save value2.sav

Opening this file on the GUI will indicate approximately 500 warnings, which is still substantial, but much better than before. Improvements to Loop analysis in the next release of Frama-C will allow this number to be reduced slightly.

The basic tutorial is over, but there are several paths to choose

From here on, there are several possibilities to reduce the imprecisions in the analysis:

  • Inspect alarms and see if their functions contain loops that were not inferred by Loop analysis; if so, adding their bounds to -slevel-function can improve the precision of the analysis;

  • Increase the precision using other parameters, such as -plevel;

  • Stub libc functions to emulate/constrain inputs when relevant;

  • Use Eva's abstract domains (e.g. -eva-equality-domain) to improve precision;

  • Stop at the first few alarms (-val-stop-at-nth-alarm), to track more closely the sources of imprecision. However, when there are hundreds of alarms, this is more useful as a learning experience than as a practical solution.

Each solution is more appropriate in a specific situation. Here are a few tips for an intermediate-level user of Eva:

  1. Functions that perform array initialization are often simple (a loop with a few assignments per iteration), so unrolling them completely should not slow down the analysis excessively. The Loop analysis plug-in usually works with them, but some pattern variations may throw it off. You may want to check the proposed values in such loops. Because initialization happens early in program execution, checking such loops may yield good results.

  2. The plevel parameter is often used in response to messages such as:

    monocypher.c:491:[kernel] more than 200(255) elements to enumerate. Approximating.

    where the first number is the current plevel (by default, 200), and the second number is the amount that would be required to avoid the approximation. In this case, -plevel 255 would be reasonable, but if you had more than 200(67108864) elements, for instance, it would not be helpful to set the plevel to such a high value.

  3. Stubbing is a good approach when dealing with functions that are closely system-dependent, specifically input functions that read from files, sockets, or from the command-line. Check the Frama-C builtins in __fc_builtin.h, they provide some useful primitives for abstracting away code with non-deterministic functions.

  4. Eva's domains have specific trade-offs between precision and efficiency, and some have broader applicability than others. Future posts in this blog will describe some of these domains, but as a rule of thumb, two domains that are fairly low-cost and generally useful are -eva-equality-domain (for syntactic equalities) and -eva-gauges-domain (for some kinds of loops).

  5. The Messages panel in the GUI is chronologically sorted, so it can help the user follow what the analysis did, to try and identify sources of imprecision. However, even in this case, there is still an advantage to using -val-stop-at-nth-alarm: because the execution stops abruptly, there are possibly less callstacks displayed in the GUI, and therefore it may be easier to see at a glance which parts of the code were actually executed, and the dependencies between values that lead to the alarm.

Non-terminating function?

The "beginner" tutorial ends here, but one thing that you may have noticed after running Eva, is the dreaded "non terminating function" message at the end of the analysis:

[value:final-states] Values at end of function main:

This indicates that, somewhere during the analysis, a completely invalid state was found, and Eva could not proceed. This usually indicates one of the following:

  1. Eva's setup is incorrect: most likely, some function has missing or incorrect specifications, or some case that cannot be currently handled by Eva (e.g. recursive calls) was encountered.
  2. A definitively undefined behavior is present in the code, which may or may not lead to an actual bug during execution. In either case, it should be taken care of.

We will see how to handle such situations in the next post, using the GUI and the Nonterm plug-in (-nonterm), in a tutorial destined for beginners and experienced users alike.

Tuesday, March 7 2017

A simple Eva tutorial, part 1

(with the collaboration of T. Antignac, Q. Bouillaguet, F. Kirchner and B. Yakobowski)

This is the first of a series of posts on a new Eva tutorial primarily aimed at beginners (some of the later posts contain more advanced content).

Reminder: Eva is the new name of the Value analysis plug-in.

There is a Value tutorial on Skein-256 that is part of the Value Analysis user manual. The present tutorial is complementary and presents some new techniques available in Frama-C. If you intend to use Eva, we recommend you read the Skein-256 tutorial as well because it details several things that will not be repeated here. (However, it is not required to have read the Skein-256 before this one.)

The source code used in this tutorial is the version 0.3 of Monocypher, a C99-conformant cryptographic library that also includes a nice test suite.

Note: newer versions of Monocypher are available! For this tutorial, please ensure you download version 0.3, otherwise you will not obtain the same behavior as described in this tutorial.

Future posts will include more advanced details, useful for non-beginners as well, so stay tuned!

Starting with Frama-C/Eva

This tutorial will use Monocypher's code, but it should help you to figure out how to analyze your code as well. First and foremost, it should help you answer these questions:

  1. Is my code suitable for a first analysis with Frama-C/Eva?
  2. How should I proceed?

(Un)Suitable code

There are lots of C code in the wild; for instance, searching Github for language:C results in more than 250k projects. However, many of them are not suitable candidates for a beginner, for reasons that will be detailed in the following.

Note that you can analyze several kinds of codes with Frama-C/Eva. However, without previous experience, some of them will raise many issues at the same time, which can be frustrating and inefficient.

Here is a list of kinds of code that a Frama-C/Eva beginner should avoid:

  1. Libraries without tests

    Eva is based on a whole-program analysis. It considers executions starting from a given entry point. Libraries without tests contain a multitude of entry points and no initial context for the analysis. Therefore, before analyzing them, you will have to write your own contexts1 or test cases.

  2. Command-line tools that rely heavily on the command-line (e.g. using getopt), without test cases.

    Similar to the previous situation: a program that receives all of its input from the command-line behaves like a library. Command-line parsers and tools with complex string manipulation are not the best use cases for the Eva's current implementation. A fuzzer might be a better tool in this case (though a fuzzer will only find bugs, not ensure their absence). Again, you will have to provide contexts1 or test cases.

  3. Code with lots of non-C99 code (e.g. assembly, compiler extensions)

    Frama-C is based on the C standard, and while it includes numerous extensions to handle GCC and MSVC-specific code, it is a primarily semantic-based tool. Inline assembly is supported syntactically, but its semantics needs to be given via ACSL annotations. Exotic compiler extensions are not always supported. For instance, trying to handle the Linux kernel without previous Frama-C experience is a daunting task.

  4. Code relying heavily on libraries (including the C standard library)

    Frama-C ships with an annotated standard library, which has ACSL specifications for many commonly-used functions (e.g. string.h and stdlib.h). This library is however incomplete and in some cases imprecise2. You will end up having to specify and refine several functions.

1 A context, here, is similar to a test case, but more general. It can contain, for instance, generalized variables (e.g. by using Frama_C_interval or ACSL specifications).

2 A balance is needed between conciseness (high-level view), expressivity, and precision (implementation-level details). The standard library shipped with Frama-C tries to be as generic as possible, but for specific case studies, specialized specifications can provide better results.

Each new version of Frama-C brings improvements concerning these aspects, but we currently recommend you try a more suitable code base at first. If your objective is to tackle such a challenging code base, contact us! Together we can handle such challenges more efficiently.

This explains why Monocypher is a good choice: it has test cases, it is self-contained (little usage of libc functions), and it is C99-conforming.

The 3-step method

In a nutshell, the tutorial consists in performing three steps:

  1. Parsing the code (adding stubs if necessary);
  2. Running Eva with mostly default parameters (for a first, approximated result);
  3. Tuning Eva and running it again.

The initial parsing is explained in this post, while the other steps will be detailed in future posts.

General recommendations

Before starting the use of Frama-C, we have some important general recommendations concerning the Eva plug-in:

  1. DO NOT start with the GUI. Use the command-line. You should consider Frama-C/Eva as a command-line tool with a viewer (the GUI). The Frama-C GUI is not an IDE (e.g. you cannot edit code with it), and Eva does not use the GUI for anything else other than rendering its results.

  2. Use scripts. Even a simple shell script, just to save the command-line options, is already enough for a start. For larger code bases, you will want Makefiles or other build tools to save time.

  3. Use frama-c -kernel-help (roughly equivalent to the Frama-C manpage) and frama-c -value-help to obtain information about the command-line options. Each option contains a brief description of what it does, so grepping the output for keywords (frama-c -kernel-help | grep debug for instance) is often useful. Otherwise, consider Stack Overflow - there is a growing base of questions and answers available there.

  4. Advance one step at a time. As you will see, the very first step is to parse the code, and nothing else. One does not simply run Eva, unless he or she is very lucky (or the program is very simple). Such precautions may seem excessive at first, but being methodical will save you time in the long run.

Parsing the code

Often overlooked, this step is erroneously considered as "too simple" ("just give all files to the command-line!"). In a few cases, it is indeed possible to run frama-c *.c -val and succeed in parsing everything and running Eva.

When this does not work, however, it is useful to isolate the steps to identify the error. Here are some general recommendations:

  1. Start with few files, and include more when needed

    Note that parsing may succeed even if some functions are only declared, but not defined. This will of course prevent Eva from analyzing them. If so, you may have to return to this step later, adding more files to be parsed.

  2. Ensure that preprocessor definitions and inclusions are correct

    Several code bases require the use of preprocessor definitions (-D in GCC) or directory inclusions (-I in GCC) in order for the code to be correctly preprocessed. Such information is often available in Makefiles, and can be given to Frama-C using e.g. -cpp-extra-args="-DFOO=bar -Iheaders".

    -cpp-extra-args is the most useful option concerning this step. It is used in almost every case study, and often the only required option for parsing. Note: old releases of Frama-C did not have this option, and -cpp-command was recommended instead. Nowadays, -cpp-command is rarely needed and should be avoided, because it is slightly more complex to use.

  3. Make stubs for missing standard library definitions

    Frama-C's standard library is incomplete, especially for system-dependent definitions that are not in C99 or in POSIX. Missing constants, for instance, may require the inclusion of stub files (e.g. stubs.h) with the definitions and/or the ACSL specifications. A common way to include such files is to use GCC's -include option, documented here.

  4. Save the result

    Use Frama-C's -save/-load options to avoid having to reparse the files each time. There is no default extension associated with Frama-C save files, although .sav is a common choice. For instance, running:

    frama-c <parse options> -save parsed.sav

    will try to parse the program and, if it succeeds, will save the Frama-C session to parsed.sav. You can then open it in the GUI (frama-c-gui -load parse.sav), to see what the normalized source code looks like, or use it as an input for the next step.

Reminder: for the Eva plug-in, the GUI is not recommended for parametrizing/tuning an analysis. It is best used as a viewer for the results.

The default output of Eva is rather verbose but very useful for studying small programs. For realistic case studies, however, you may want to consider the following options:

  • -no-val-show-progress: does not print when entering a new function. This will be the default in Frama-C 15 (Phosphorus);

  • -value-msg-key=-initial-state: does not print the initial state;

  • -value-msg-key=-final-states: does not print the final states of the analysis.

Note the minus symbols (-) before initial-state and final-states. They indicate we want to hide the messages conditioned by these categories.

Parsing monocypher

As indicated above, the naive approach (frama-c *.c) does not work with monocypher:

$ frama-c *.c

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing monocypher.c (with preprocessing)
[kernel] Parsing more_speed.c (with preprocessing)
[kernel] syntax error at more_speed.c:15:
         14    // Specialised squaring function, faster than general multiplication.
         15    sv fe_sq(fe h, const fe f)
         16    {
         17        i32 f0 = f[0]; i32 f1 = f[1]; i32 f2 = f[2]; i32 f3 = f[3]; i32 f4 = f[4];

The first line is always printed when Frama-C parses a source file, and can be ignored.

The second line indicates that monocypher.c is being parsed.

The third line indicates that more_speed.c is now being parsed, implying that the parsing of monocypher.c ended without issues.

Finally, we have a parsing error in more_speed.c, line 15. That line, plus the lines above and below it, are printed in the console.

Indeed, the file more_speed.c is not a valid C source (sv is not a type defined in that file, and it does not include any other files). But this is not an actual issue, since more_speed.c is not part of the library itself, simply an extra file (this can be confirmed by looking into the makefile). Thus we are going to restrict the set of files Frama-C is asked to analyze.

Note: Frama-C requires the entire program to be parsed at once. It may be necessary to adapt compilation scripts to take that into account.

We also see that the rule for building monocypher.o includes a preprocessor definition, -DED25519_SHA512. We will add that to our parsing command, which will then become:

frama-c test.c sha512.c monocypher.c -cpp-extra-args="-DED25519_SHA512" -save parsed.sav

The lack of error messages is, in itself, a resounding success.

The first part of this tutorial ends here. See you next week!

For now, you can start reading the Skein-256 tutorial available at the beginning of the Eva manual. Otherwise, if you already know Eva (and still decided to read this), you may try to find some undefined behavior (UB) in Monocypher 0.3!

Hint: There is indeed some UB, although it does not impact the code in any meaningful way. At least not with today's compilers, maybe in the future... and anyway, it has been fixed in the newer releases of Monocypher.

Tuesday, December 13 2016

Frama-C Silicon has been released!

Frama-C 14 (Silicon) has just been released. In this post, we present a few additions that should help everyday usage of Value EVA.

Value is now EVA

The Value analysis plug-in has been renamed EVA, for Evolved Value Analysis. It has a new architecture that allows plugging abstract domains, among other features. It is a truly remarkable evolution which this post is too small to contain1, however, so it will presented in more detail later.

1 Facetious reference to Fermat's Last Theorem

Automatic built-in matching for libc functions

One of the new user-friendly features is the -val-builtins-auto option, which avoids having to memorize which built-in to use for each libc function that has one, namely malloc, free, and some floating-point and string-related functions (e.g. pow and strlen).

For instance, consider the following toy program, which simply allocates a buffer, copies a string into it, then allocates a buffer of the right size for the string, and stores it there.

// file.c
#include <stdio.h>
#include <stdlib.h>
#include "string.c" // include Frama-C's implementation of string.h

int main() {
  char *buf = malloc(256); // allocate a large buffer
  if (!buf) exit(1);
  char *msg = "silicon";
  strcpy(buf, msg);
  size_t n = strlen(buf);
  char *str = malloc(n + 1); // allocate a buffer with the exact size (plus '\0')
  if (!str) exit(1);
  strncpy(str, buf, n);
  str[n] = 0;
  size_t n2 = strlen(str);
  //@ assert n == n2;
  return 0;

This program uses dynamic allocation and calls functions from string.h.

The following command-line is enough to obtain an interesting result:

frama-c file.c -val -val-builtins-auto -slevel 7

Without -val-builtins-auto one would need to use this overly long argument:

-val-builtin malloc:Frama_C_alloc_by_stack,free:Frama_C_free,strlen:Frama_C_strlen

For more details about Frama_C_alloc_by_stack, check the EVA manual, section 8.1.

The builtins for free and strlen were automatically chosen by EVA. Note however that strcpy and strncpy do not have builtins. In this case, we include "string.c" (which is actually in share/libc/string.c) to use the implementations available with Frama-C.

Analyzing a program using the implementations in share/libc/string.c is less efficient than using a built-in, but more precise than using only a specification. These implementations are designed to minimize the number of alarms when their inputs are imprecise. Also, because they are not optimized for execution, they are conceptually simpler than the actual libc implementations.

Using these functions. -slevel 7 ensures that their loops are fully unrolled in the example. Can you guess why 7 is the right value here?

Inspecting values in the GUI

Another improvement to usability comes in the form of a popup menu in the GUI. To see it, run the following command using the same file as previously:

frama-c-gui file.c -val -val-builtins-auto -slevel 7

On the Frama-C GUI, click on the str expression in the statement str = (char *)malloc(n + (size_t)1); (corresponding to line 11 in the original source code). Then open the Values tab, and you will see something similar to this:

Show pointed values in the GUI

In the Values tab on the bottom, right-clicking on the cell containing the NULL; &__malloc_main_l11[0] value will show a popup menu "Display values for ...". Clicking on it will add a new column displaying its contents.

Before Silicon, this information was already available, but as the result of a long and painful process. The new popup menu shows one entry per pointed variable in the chosen cell, so if there are several different values, there will be several popup menu entries.

malloc may fail

In the previous example, the values of str are those returned by the malloc builtin: NULL and a newly allocated base (__malloc_main_l11). This models the fact that there may not be enough memory, and malloc may fail. The code should definitely handle this case! But for the hurried evaluator, the use of option -no-val-malloc-returns-null can help focus on the other potential run-time errors (before coming back to the malloc-related ones).

Still ways to go

In this example, there are still some warnings, due to the specification of functions strcpy and strncpy, which use logical constructs not yet evaluated by EVA (but very useful for WP). They are not an issue in this example, since we used the actual implementation of these functions, and therefore do not need their specifications, but future work on EVA will help deal with these details and provide a more streamlined experience.

Tuesday, November 22 2016

Frama-C and ACSL are on GitHub

We are glad to announce the creation of official GitHub repositories for Frama-C and ACSL, to stimulate contributions from the community, and to better contribute back to it.

Frama-C is on GitHub

Frama-C now (in fact, since a few months) has an official GitHub repository:

It contains snapshots of each Frama-C release, starting from Hydrogen all the way up to Aluminium. It also contains a branch for release candidates.

Issues and pull requests can be submitted via GitHub, for those who prefer it to MantisBT's interface (which remains the official Frama-C bug tracker).

ACSL is also on GitHub

On a related note, a new repository for the ACSL documentation has also been created:

Previously, documentation issues (typos, updates, etc.) had to be reported to the Frama-C bug tracking system, which was not ideal, since ACSL is not part of Frama-C, even if Frama-C is currently ACSL's largest user.

This new repository, which is now the official channel for the ACSL language specification, will help evolve it, by giving contributors direct access to the source code, and allowing faster creation of issues and pull requests with updates (typos, corrections, etc.).

Wednesday, October 12 2016

A mini ACSL tutorial for Value, part 3: indirect assigns

To conclude our 3-part series on ACSL specifications for Value, we present a feature introduced in Frama-C Aluminium that allows more precise specifications: the indirect label in ACSL assigns clauses. The expressivity gains when writing \froms are especially useful for plugins such as Value.

Indirect assigns

Starting in Frama-C Aluminium (20150601), assigns clauses (e.g. assigns x \from src) accept the keyword indirect (e.g. assigns x \from indirect:src), stating that the dependency from src to x is indirect, that is, it does not include data dependencies between src and x. In other words, src itself will never be directly assigned to x.

Indirect dependencies are, most commonly, control dependencies, in which src affects x by controlling whether some instruction will modify the value of x. Another kind of indirect dependency are address dependencies, related to the computation of addresses for pointer variables.

Let us once again refer to our running example, the specification and mock implementation of safe_get_random_char. As a reminder, here's its specification, without the ensures \subset(*out,...) postcondition, as suggested in the previous post:

#include <stdlib.h>
typedef enum {OK, NULL_PTR, INVALID_LEN} status;

  assigns \result \from out, buf, n;
  assigns *out \from out, buf, buf[0 .. n-1], n;
  behavior null_ptr:
    assumes out == \null || buf == \null;
    assigns \result \from out, buf, n;
    ensures \result == NULL_PTR;
  behavior invalid_len:
    assumes out != \null && buf != \null;
    assumes n == 0;
    assigns \result \from out, buf, n;
    ensures \result == INVALID_LEN;
  behavior ok:
    assumes out != \null && buf != \null;
    assumes n > 0;
    requires \valid(out);
    requires \valid_read(&buf[0 .. n-1]);
    ensures \result == OK;
    ensures \initialized(out);
  complete behaviors;
  disjoint behaviors;
status safe_get_random_char(char *out, char const *buf, unsigned n);

Here's the mock implementation of the original function, in which ensures \subset(*out,...) holds:

#include "__fc_builtin.h"
#include <stdlib.h>
typedef enum { OK, NULL_PTR, INVALID_LEN } status;

status safe_get_random_char(char *out, char const *buf, unsigned n) {
  if (out == NULL || buf == NULL) return NULL_PTR;
  if (n == 0) return INVALID_LEN;
  *out = buf[Frama_C_interval(0,n-1)];
  return OK;

And here's the main function used in our tests:

void main() {
  char *msg = "abc";
  int len_arr = 4;
  status res;
  char c;
  res = safe_get_random_char(&c, msg, len_arr);
  //@ assert res == OK;
  res = safe_get_random_char(&c, NULL, len_arr);
  //@ assert res == NULL_PTR;
  res = safe_get_random_char(NULL, msg, len_arr);
  //@ assert res == NULL_PTR;
  res = safe_get_random_char(&c, msg, 0);
  //@ assert res == INVALID_LEN;

In the mock implementation, we see that out and buf are tested to see if they are equal to NULL, but their value itself (i.e., the address they point to) is never actually assigned to *out; only the characters inside buf may be assigned to it. Therefore, out and buf are both control dependencies (in that, they control whether *out = buf[Frama_C_interval(0,n-1)] is executed), and thus indirect as per our definition.

n is also a control dependency of the assignment to *out, due to the check if (n == 0). n also appears in buf[Frama_C_interval(0,n-1)], leading this time to an address dependency: in lval = *(buf + Frama_C_interval(0,n-1)), lval depends indirectly on every variable used to compute the address that will be dereferenced (buf, n, and every variable used by Frama_C_interval in this case).

If we run Value using our specification, this is the result:

[value] ====== VALUES COMPUTED ======
[value] Values at end of function main:
  msg ∈ {{ "abc" }}
  len_arr ∈ {4}
  res ∈ {2}
  c ∈
   {{ garbled mix of &{c; "abc"}
    (origin: Arithmetic {file.c:33}) }}

Note that c has a garbled mix which includes c itself, plus the string literal "abc". The culprit is this assigns clause:

assigns *out \from out, buf, buf[0 .. n-1], n;

out is c and buf is "abc". n, despite also being a dependency, does not contribute to the garbled mix because it is a scalar. The garbled mix appears because, in some functions, it is the address of the pointer itself that is assigned to the lvalue in the assigns clause. Without a means of distinguishing between direct and indirect dependencies, one (dangerous) workaround is to omit some dependencies from the clauses. This may lead to incorrect results.

Thanks to indirect \from clauses, now we can avoid the garbled mix by specifying that out and buf are only indirect dependencies. Applying the same principle to all assigns clauses, we obtain the final version of our (fixed) specification:

  assigns \result \from indirect:out, indirect:buf, indirect:n;
  assigns *out \from indirect:out, indirect:buf, buf[0 .. n-1], indirect:n;
  behavior null_ptr:
    assumes out == \null || buf == \null;
    assigns \result \from indirect:out, indirect:buf, indirect:n;
    ensures \result == NULL_PTR;
  behavior invalid_len:
    assumes out != \null && buf != \null;
    assumes n == 0;
    assigns \result \from indirect:out, indirect:buf, indirect:n;
    ensures \result == INVALID_LEN;
  behavior ok:
    assumes out != \null && buf != \null;
    assumes n > 0;
    requires \valid(out);
    requires \valid_read(&buf[0 .. n-1]);
    ensures \result == OK;
    ensures \initialized(out);
  complete behaviors;
  disjoint behaviors;
status safe_get_random_char(char *out, char const *buf, unsigned n);

Note that indirect dependencies are implied by direct ones, so they never need to be added twice.

With this specification, Value will return c ∈ [--..--], without garbled mix. The result is still imprecise due to the lack of ensures, but better than before. Especially when trying Value on a new code base (where most functions have no stubs, or only simple ones), the difference between garbled mix and [--..--] (often called top int, that is, the top value of the lattice of integer ranges) is significant.

In the new specification, it is arguably easier to read the dependencies and to reason about them: users can skip the indirect dependencies when reasoning about the propagation of imprecise pointer values.

The new specification is more verbose because indirect is not the default. And this is so in order to avoid changing the semantics of existing specifications, which might become unsound.

The From plugin has a new (experimental) option, --show-indirect-deps, which displays the computed dependencies using the new syntax. It is considered experimental simply because it has not yet been extensively used in industrial applications, but it should work fine. Do not hesitate to tell us if you have issues with it.

Ambiguously direct dependencies

It is not always entirely obvious whether a given dependency can be safely considered as indirect, or if it should be defined as direct. This is often the case when a function has an output argument that is related to the length (or size, cardinality, etc.) of one of its inputs. strnlen(s, n) is an example of a libc function with that property: it returns n itself when s is longer than n characters.

Let us consider the following function, which searches for a character in an array and returns its offset, or the given length if not found:

// returns the index of c in buf[0 .. n-1], or n if not found
/*@ assigns \result \from indirect:c, indirect:buf,
                          indirect:buf[0 .. n-1], indirect:n; */
int indexOf(char c, char const *buf, unsigned n);

Our specification seems fine: the result value is usually the number of loop iterations, and therefore it depends indirectly on the related arguments.

However, the following implementation contradicts it:

int indexOf(char c, char const *buf, unsigned n) {
  unsigned i;
  for (i = 0; i < n; i++) {
    if (buf[i] == c) return i;
  return n;

void main() {
  int i1 = indexOf('a', "abc", 3);
  int i2 = indexOf('z', "abc", 3);

If we run frama-c -calldeps -show-indirect-deps (that is, run the From plugin with callwise dependencies, showing indirect dependencies) in this example, we will obtain this output:

[from] call to indexOf at ambiguous.c:10 (by main):
  \result FROM indirect: c; buf; n; "abc"[bits 0 to 7]
[from] call to indexOf at ambiguous.c:11 (by main):
  \result FROM indirect: c; buf; n; "abc"[bits 0 to 23]; direct: n
[from] entry point:

Note that, in the second call, n is computed as a direct dependency. Indeed, it is directly assigned to the return value in the code. This means that our specification is possibly unsound, since it states that n is at most an indirect dependency of \result.

However, if we modify our implementation of indexOf to return i instead of n, then From will compute n as an indirect dependency, and thus our specification could be considered correct. The conclusion is that, in some situations, both versions can be considered correct, and this not will affect the end result.

One specific case where such discussions may be relevant is the case of the memcmp function of the C standard library (specified in string.h): one common implementation consists in comparing each byte of both arrays, say s1[i] and s2[i], and returning s1[i] - s2[i] if they are different. One could argue that such an implementation would imply that assigns \result \from s1[0 ..], s2[0 ..], with direct dependencies. However, this can create undesirable garbled mix, so a better approach would be to consider them as indirect dependencies. In such situations, the best specification is not a clear-cut decision.

Frama-C libc being updated

The Frama-C stdlib has lots of specifications that still need to be updated to take indirect into account. This is being done over time, which means that unfortunately they do not yet constitute a good example of best practices. This is improving with each release, and soon they should offer good examples for several C standard library functions. Until then, you may refer to this tutorial or ask the Frama-C community for recommendations to your specifications.

Also note that some of these recommendations may not be the most relevant ones when considering other plugins, such as WP. Still, most tips here are sufficiently general that they should help you improve your ACSL for all purposes.

Friday, September 30 2016

A mini ACSL tutorial for Value, part 2: functional dependencies

In our previous post, we left you in a cliffhanger: which \from is missing from our ACSL specification for safe_get_random_char? In this post, we explain the functional dependencies in our specification, how to test them, and then present the missing dependency.

Where do the \from come from?

Our complete specification for safe_get_random_char in the previous post includes several functional dependencies. Some of them are obvious, others not so much. For easier reference, here is the specification once again:

#include <stdlib.h>
typedef enum {OK, NULL_PTR, INVALID_LEN} status;

  assigns \result \from out, buf, n;
  assigns *out \from out, buf, buf[0 .. n-1], n;
  behavior null_ptr:
    assumes out == \null || buf == \null;
    assigns \result \from out, buf, n;
    ensures \result == NULL_PTR;
  behavior invalid_len:
    assumes out != \null && buf != \null;
    assumes n == 0;
    assigns \result \from out, buf, n;
    ensures \result == INVALID_LEN;
  behavior ok:
    assumes out != \null && buf != \null;
    assumes n > 0;
    requires \valid(out);
    requires \valid_read(&buf[0 .. n-1]);
    ensures \result == OK;
    ensures \initialized(out);
    ensures \subset(*out, buf[0 .. n-1]);
  complete behaviors;
  disjoint behaviors;
status safe_get_random_char(char *out, char const *buf, unsigned n);

As a reminder, assigns a \from b1, b2, ... specifies that there are control and/or data dependencies from b1, b2, ... to a. Data dependencies are direct or indirect assignments (e.g. a = b1 or c = b1; a = c), and control dependencies are related to control-flow (e.g. if (b1 && b2) { a = 1; } else { a = 2; }). Value uses them for several purposes, such as:

  • precision: to define the possible origins of pointers, otherwise imprecise values will degenerate into "modifies anything";
  • efficiency: to avoid recomputing the state during a leaf function call, if the only difference is in the values of variables that no one depends on.

Value always requires that assigns clauses contain \from dependencies. Since \from are an overapproximation of the actual dependencies, in case of doubt the safe bet is to include more than the necessary. Too many \from, however, may lead to imprecise analyses.

One way to consider whether a given location should be part of a \from is to think in terms of variation: if the actual value of the location changed, would it possibly affect the assigned lvalue? If so, then there is a dependency.

Let us revisit our first get_random_char function, in particular its assigns clause:

//@ assigns \result \from buf[0 .. n-1], n;
char get_random_char(char const *buf, unsigned n);

If we change the value of any character between buf[0] and buf[n-1], this can have a direct impact on the result. Changing the value of n obviously also has an effect: there are more characters to choose from.

However, one thing that does not affect the result is the address of buf itself, that is, the contents of the buf pointer: if the buffer starts on address 0x42, or on address 0xfffe1415, the result of the function is the same, as long as the precondition is valid (i.e., the memory location is readable) and the contents of the buffer are the same.

But why, then, do we have buf (the pointer, not the pointed value) as part of the \from in safe_get_random_char (copied below)?

//@ assigns \result \from out, buf, n;
status safe_get_random_char(char *out, char const *buf, unsigned n);

Note that out is also present as a dependency, and for the same reason: the NULL pointer. In our specification, we included assumes clauses such as out == \null || buf == \null. We may expect, therefore, that our function will be able to distinguish whether any of these pointers is null, very likely via a test such as the following:

if (out == NULL || buf == NULL) { return INVALID_LEN; }

Such a test introduces control dependencies between out, buf and \result: if out is 0, the result is different than if out is nonzero (i.e. non-null). For that reason, out and buf must be included as dependencies. Conversely, note that the contents of the buffer itself do not affect \result.

When in doubt, try some code

A good way to check a specification is (when possible) to write an abstracted code of the function under test, then run Value (and sometimes From) and see if it matches the expectations.

For safe_get_random_char, a few lines of code suffice to obtain a roughly equivalent version of our specification:

#include "__fc_builtin.h"
#include <stdlib.h>
typedef enum { OK, NULL_PTR, INVALID_LEN } status;

status safe_get_random_char(char *out, char const *buf, unsigned n) {
  if (out == NULL || buf == NULL) return NULL_PTR;
  if (n == 0) return INVALID_LEN;
  *out = buf[Frama_C_interval(0,n-1)];
  return OK;

Note the usage of the built-in Frama_C_interval (included via __fc_builtin.h) to simulate a random value between 0 and n-1 (inclusive).

Now we need a main function to invoke our code. We will reuse the one we defined before, since its calls activate all branches in our code. Re-running Value, this time using the code plus the specification, will prove all pre- and post-conditions, except the one related to \subset(*out, buf[0 .. n-1]). This is just an imprecision in Value that may disappear in the future.

We can also try running the From plugin (frama-c -deps), without our specification, to see if the dependencies it infers are compatible with the ones we specified in our assigns clauses.

For function safe_get_random_char, From will infer the following dependencies related to \result and *out:

  a FROM Frama_C_entropy_source; out; buf; n; "abc" (and SELF)
  \result FROM out; buf; n

Frama_C_entropy_source comes from the usage of Frama_C_interval. For now, let us focus on the other variables:

  • a is actually *out, and "abc" is actually buf[0 .. n-1]. The result of the From plugin is very concrete, so we have to abstract a few variable names.
  • the SELF dependence related to *out simply means that the variable may not be assigned in the function (e.g. when an error is found). This information is not present in assigns clauses. In particular, for Value it could be useful to have a "must assign" clause, describing an underapproximation of assignments that are certain to happen in every execution. This is not present in ACSL, but it can often be compensated with the use of behaviors with refined assigns and ensures clauses, as we did.
  • all dependencies, both for *out and \result, are the ones we had predicted before, except for Frama_C_entropy_source.

Variables such as Frama_C_entropy_source are often used to represent internal states of elements that are abstracted away in specifications. In this case, it can be seen as the internal state of the (pseudo-)random number generator that allows the result of our safe_get_random_char to be non-deterministic. Without it, we would have a function that could be assumed to return the same value every time that the same input parameters were given to it.

Thus, to really model a randomized result, we need to add such a variable to our specification. It is important not to forget to also assign to the variable itself, to represent the fact that its own internal state changed during the call. In our specification, it would be sufficient to add the following line to the global assigns clause:

  assigns Frama_C_entropy_source \from Frama_C_entropy_source;

With this final assigns clause, our specification is indeed complete. This concludes our tutorial on ACSL specifications oriented towards an analysis with Value!

A minor variant, an unexpected result

Let us consider a minor variant of our specification: what if we remove the postcondition ensures \subset(*out, buf[0 .. n-1])? We would expect Value to return [--..--], since *out is said to be assigned by the function, but we did not specify which values it may contain. However, this is what we obtain instead, after the call to safe_get_random_char(&c, msg, len_msg):

  c ∈
   {{ garbled mix of &{c; "abc"} (origin: Arithmetic {file.c:44}) }}

This undesirable garbled mix indicates that some pointer information leaked to the contents of the variable c, more precisely, that the address of c (out) itself could be contained in c. We know this is not the case, since in every reasonable implementation of safe_get_random_char, the address of out is never directly assigned to *out. However, until Frama-C Magnesium, there was no way to specify the distinction between dependencies that may impact the actual contents of an lvalue from dependencies which are only indirectly related to its value (e.g. control dependencies, such as testing whether out is NULL or not).

Because of that limitation, there were typically two ways to deal with that: omit dependencies (dangerous!) or accept the introduction of garbled mix. Frama-C Aluminium brought a new way to handle them that solves both issues. This will be the subject of the next post in this blog. Stay tuned!

Friday, September 23 2016

A mini-tutorial of ACSL specifications for Value

(with the collaboration of F. Kirchner, V. Prevosto and B. Yakobowski)

Users of the Value plugin often need to use functions for which there is no available code, or whose code could be abstracted away. In such cases, ACSL specifications often come in handy. Our colleagues at Fraunhofer prepared the excellent ACSL by example report, but it is mostly directed at WP-style proofs.

In this post we explain how to specify in ACSL a simple function, in a way that is optimal for Value.


  • Basic knowledge of Value;
  • Basic knowledge of ACSL.

The messages and behaviors presented here are those of Frama-C Aluminium. Using another version of Frama-C might lead to different results.

A simple function

In this tutorial, we proceed in a gradual manner to isolate problems and make sure that each step works as intended. Let us consider the following informal specification:

// returns a random character between buf[0] and buf[n-1]
char get_random_char(char const *buf, unsigned n);

A minimal ACSL specification for this function must check two things:

  1. that n is strictly positive: otherwise, we'd have to select a character among an empty set, thereby killing any logician that would wander around at that time (buf is a byte array that may contain \0, so that there is no obvious way to return a default value in case n == 0);
  2. that we are allowed (legally, as per the C standard) to read characters between buf[0] and buf[n-1];

The following specification ensures both:

  requires n > 0;
  requires \valid_read(buf+(0 .. n-1));
char get_random_char(char const *buf, unsigned n);

Note the spaces between the bounds in 0 .. n-1. A common issue, when beginning to write ACSL specifications, is to write ranges such as 0..n-1 without spaces around the dots. It works in most cases, but as 0..n is a floating-point preprocessing token (yes, this looks strange, but you can see it yourself in section 6.4.8 of C11 standard if you're not convinced) funny things might happen when pre-processing the annotation. For instance, if we had a macro MAX instead of n, (e.g. #define MAX 255), then writing [0..MAX] would result in the following error message: [kernel] user error: unbound logic variable MAX, since the pre-processor would dutifully consider 0..MAX as a single token, thus would not perform the expansion of MAX. For that reason, we recommend always writing ranges with spaces around the dots.

To check our specification, we devise a main function that simply calls get_random_char with the appropriate arguments:

void main() {
  char *buf = "abc";
  char c = get_random_char(buf, 3);

Then, if we run this with Value (frama-c -val), it will produce the expected result, but with a warning:

[kernel] warning: No code nor implicit assigns clause for function get_random_char, generating default assigns from the prototype

By printing the output of Frama-C's normalisation (frama-c -print), we can see what its generated assigns clause looks like:

assigns \result;
assigns \result \from *(buf+(0 ..)), n;

Despite the warning, Frama-C kernel generated a clause that is correct and not too imprecise in this case. But we should not rely on that and avoid this warning whenever possible, by writing our own assigns clauses:

  requires n > 0;
  requires \valid_read(buf+(0 .. n-1));
  assigns \result \from buf[0 .. n-1], n;
char get_random_char(char const *buf, unsigned n);

Running Value again will not emit any warnings, plus it will indicate that both preconditions were validated:

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing file.c (with preprocessing)
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization

[value] computing for function get_random_char <- main.
        Called from file.c:10.
[value] using specification for function get_random_char
file.c:2:[value] function get_random_char: precondition got status valid.
file.c:3:[value] function get_random_char: precondition got status valid.
[value] Done for function get_random_char
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function main:
  buf ∈ {{ "abc" }}
  c ∈ [--..--]

However, the result is still imprecise: c ∈ [--..--], that is, it may contain any character, not only 'a', 'b' or 'c'. This is expected: assigns \from ... clauses are used by Value to compute dependencies information, but they are not sufficient to constrain the exact contents of the assigned variables. We need to use postconditions for that, that is, ensures clauses.

The following ensures clause states that the result value must be one of the characters in buf[0 .. n-1]:

ensures \subset(\result, buf[0 .. n-1]);

The ACSL \subset predicate is interpreted by Value, which isolates the characters in buf, and thus returns a precise result: c ∈ {97; 98; 99}. Note that Value prints the result as integers, not as ASCII characters.

This concludes the specification of a very simple partial function. But what if we want to take into account more possibilities, e.g. a NULL pointer in buf, or n == 0?

First try: a robust and concise specification

Our get_random_char function is simple, but not robust. It is vulnerable to accidents and attacks. Let us apply some Postel-style recommendations and be liberal in what we accept from others: instead of expecting that the user will not pass a NULL pointer or n == 0, we want to accept these cases, but return an error code if they happen.

We have two choices: add an extra argument to get_random_char that represents the result status (OK/error), or use the return value as the status itself, and return the character via a pointer. Here, we will adopt the latter approach:

typedef enum { OK, NULL_PTR, INVALID_LEN } status;

// if buf != NULL and n > 0, copies a random character from buf[0 .. n-1]
// into *out and returns OK.
// Otherwise, returns NULL_PTR if buf == NULL, or INVALID_LEN if n == 0.
status safe_get_random_char(char *out, char const *buf, unsigned n);

We could also have used errno here, but global variables are inelegant and, most importantly, it would defeat the purpose of this tutorial, wouldn't it?

This new function is more robust to user input, but it has a price: its specification will require more sophistication.

Before revealing the full specification, let us try a first, somewhat naive approach:

typedef enum { OK, NULL_PTR, INVALID_LEN } status;

  assigns \result, *out \from buf[0 .. n-1], n;
  ensures \subset(*out, buf[0 .. n-1]);
status safe_get_random_char(char *out, char const *buf, unsigned n);

void main() {
  char *buf = "abc";
  char c;
  status res = safe_get_random_char(&c, buf, 3);
  //@ assert res == OK;

This specification has several errors, but we will try it anyway. We will reveal the errors as we progress.

Once again, we use a small C main function to check our specification, starting with the non-erroneous case. This reveals that Value does not return the expected result:

[value] Values at end of function main:
  buf ∈ {{ "abc" }}
  c ∈ [--..--] or UNINITIALIZED
  res ∈ {0}

Variable c is imprecise, despite our \ensures clause. This is due to the fact that Value will not reduce the contents of a memory location that may be uninitialized. Thus, when specifying the ensures clause of a pointed variable, it is first necessary to state that the value of that variable is properly initialized.

This behavior may evolve in future Frama-C releases. In particular, our specification could have resulted in a more precise result, such as c ∈ {97; 98; 99} or UNINITIALIZED.

Adding ensures \initialized(out); before the \ensures \subset(...) clause will allow c to be precisely reduced to {97; 98; 99}. This solves our immediate problem, but creates another: is the specification too strong? Could we have an implementation of get_random_char in which \initialized(out) does not hold?

The answer here is definitely yes, especially in the case where buf is NULL. It is arguably also the case when n == 0, although it depends on the implementation.

The most precise and correct result that we expect here is c ∈ {97; 98; 99} or UNINITIALIZED. To obtain it, we will use behaviors.

Another reason to consider using behaviors is the fact that our \assigns clause is too generic, leading to avoidable warnings by Value: because we have written that *out may be assigned, Value will try to evaluate if out is a valid pointer. If our main function includes a test such as res = safe_get_random_char(NULL, buf, 3), Value will output the following:

[value] warning: Completely invalid destination for assigns clause *out. Ignoring.

This warning is not needed here, but its presence is justified by the fact that, in many cases, it helps detect incorrect specifications, such as an extra *. Value will still accept our specification, but if we want a precise analysis, the best solution is to use behaviors to specify each case.

Second try: using behaviors

The behaviors of our function correspond to each of the three cases of enum status:

  1. NULL_PTR when either out or buf are NULL;
  2. INVALID_LEN when out and buf are not NULL but n == 0;
  3. OK otherwise.

ACSL behaviors can be named, improving readability and generating more precise error messages. We will define a set of complete and disjoint behaviors; this is not required in ACSL, but for simple functions it often matches more closely what the code would actually do, and is simpler to reason about.

One important remark is that disjoint and complete behaviors are not checked by Value. The value analysis does take them into account to improve its precision when possible, but if they are incorrectly specified, Value may not be able to warn the user about it.

Here is one way to specify three disjoint behaviors for this function, using mutually exclusive assumes clauses.

  behavior ok:
    assumes out != null && buf != \null;
    assumes n > 0;
    requires \valid_read(buf+(0 .. n-1));
    requires \valid(out);
    // TODO: assigns and ensures clauses
  behavior null_ptr:
    assumes out == \null || buf == \null;
    // TODO: assigns and ensures clauses
  behavior invalid_len:
    assumes out != \null && buf != \null;
    assumes n == 0;
    // TODO: assigns and ensures clauses
status safe_get_random_char(char *out, char const *buf, unsigned n);

Our choice of behaviors is not unique: we could have defined, for instance, two behaviors for null pointers, e.g. null_out and null_buf; but the return value is the same for both, so this would not improve precision.

Note that assumes and requires play different roles in ACSL: assumes are used to determine which behavior(s) are active, while requires impose constraints on the pre-state of the function or current behavior. For instance, one should not specify assumes \valid(out) in one behavior and assumes !\valid(out) in another: what this specification would actually mean is that the corresponding C function should somehow be able to distinguish between locations where it can write and locations where it cannot, as if one could write if (valid_pointer(buf)) in the C code. In practical terms, the main consequence is that such a specification would prevent Value from detecting errors related to memory validity.

For a more concrete example of the difference between them, you may consult the small appendix at the end of this post.

Assigns clauses in behaviors

Our specification for safe_get_random_char is incomplete: it has no assigns or ensures clauses.

Writing assigns clauses in behaviors is not always trivial, so here is a small, simplified summary of the main rules concerning the specification of such clauses for an analysis with Value:

  1. Global (default) assigns must always be present (even for complete behaviors), and must be at least as general as the assigns clauses in each behavior;
  2. Behaviors only need assigns clauses when they are more specific than the global one.
  3. Having a complete behaviors clause allows the global behavior to be ignored during the evaluation of the post-state, which may lead to a more precise result; but the global assigns must still be present.

Note: behavior inclusion is not currently checked by Value. Therefore, if a behavior's assigns clause is not included in the default one, the result is undefined.

Also, the reason why assigns specifications are verbose and partially redundant is in part because not every Frama-C plugin is able to precisely handle behaviors. They use the global assigns in this case.

For ensures clauses, the situation is simpler: global and local ensures clauses are simply merged with an implicit logical AND between them.

The following specification is a complete example of the usage of behaviors, with precise ensures clauses for both outputs (\result and out). The main function below tests each use case, and running Value results in valid statuses for all preconditions and assertions. The \from terms in the assigns clauses are detailed further below.

#include <stdlib.h>
typedef enum {OK, NULL_PTR, INVALID_LEN} status;

  assigns \result \from out, buf, n;
  assigns *out \from out, buf, buf[0 .. n-1], n;
  behavior null_ptr:
    assumes out == \null || buf == \null;
    assigns \result \from out, buf, n;
    ensures \result == NULL_PTR;
  behavior invalid_len:
    assumes out != \null && buf != \null;
    assumes n == 0;
    assigns \result \from out, buf, n;
    ensures \result == INVALID_LEN;
  behavior ok:
    assumes out != \null && buf != \null;
    assumes n > 0;
    requires \valid(out);
    requires \valid_read(&buf[0 .. n-1]);
    ensures \result == OK;
    ensures \initialized(out);
    ensures \subset(*out, buf[0 .. n-1]);
  complete behaviors;
  disjoint behaviors;
status safe_get_random_char(char *out, char const *buf, unsigned n);

void main() {
  char *msg = "abc";
  int len_arr = 4;
  status res;
  char c;
  res = safe_get_random_char(&c, msg, len_arr);
  //@ assert res == OK;
  res = safe_get_random_char(&c, NULL, len_arr);
  //@ assert res == NULL_PTR;
  res = safe_get_random_char(NULL, msg, len_arr);
  //@ assert res == NULL_PTR;
  res = safe_get_random_char(&c, msg, 0);
  //@ assert res == INVALID_LEN;

Our specification includes several functional dependencies (\from), but there is still one missing. Can you guess which one? The answer, as well as more details about why and how to write functional dependencies, will appear in the next post. Stay tuned!

Appendix: example of the difference between requires and assumes clauses

This appendix presents a small concrete example of what happens when the user mistakingly uses requires clauses instead of assumes. It is directed towards beginners in ACSL.

Consider the (incorrect) example below, where bzero_char simply writes 0 to the byte pointed by the argument c:

  assigns *c \from c;
  behavior ok:
    assumes \valid(c);
    ensures *c == 0;
  behavior invalid:
    assumes !\valid(c);
    assigns \nothing;
  complete behaviors;
  disjoint behaviors;
void bzero_char(char *c);

void main() {
  char *c = "abc";

In this example, Value will evaluate the validity of the pointer c, and conclude that, because it comes from a string literal, it may not be written to (therefore \valid(c) is false). Value then does nothing and returns, without any warnings or error messages.

However, had we written it the recommended way, the result would be more useful:

  assigns *c \from c;
  behavior ok:
    assumes c != \null;
    requires \valid(c);
    ensures *c == 0;
  behavior invalid:
    assumes c == \null;
    assigns \nothing;
  complete behaviors;
  disjoint behaviors;
void bzero_char(char *c);

void main() {
  char *c = "abc";

In this case, Value will evaluate c as non-null, and will therefore activate behavior ok. This behavior has a requires clause, therefore Value will check that memory location c can be written to. Because this is not the case, Value will emit an alarm:

[value] warning: function bzero_char, behavior ok: precondition got status invalid.

Note that checking whether c is null or non-null is something that can be done in the C code, while checking whether a given pointer p is a valid memory location is not. As a rule of thumb, conditions in the code correspond to assumes clauses in behaviors, while requires clauses correspond to semantic properties, function prerequisites that cannot necessarily be tested by the implementation.

- page 1 of 24