--- layout: post author: Andre title: 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 fdopens
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.
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-ACSLs instrumentation.
Note that, due to the usage of jemalloc
and some technical details, E-ACSL
is disabled by default in Mac and Windows.
#include
directivesOne 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:
#include
directives are present at the beginning of the file. Theseerrno.h
is present because Frama-Cs stdio.h
includes it. As you can see,printf_va_1
is visible. This is due to the fact thatprintf_va_1
is a specific instantiation of theprintf
function. You can disable the automatic variadic translation-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.
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:
CPPFLAGS
, FCFLAGS
EVAFLAGS
to delineate which options are related to preprocessing,frama-c -load <target>.eva/framac.sav ...
).Note, however, that there are some caveats concerning this repository:
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.