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 (note: this has been renamed analysis-scripts in newer releases) 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.