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-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.
#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-C’s 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.
Sed ut perspiciatis unde omnis iste natus error sit voluptatem accusantium doloremque laudantium, totam rem aperiam, eaque ipsa quae ab illo inventore veritatis et quasi architecto beatae vitae dicta sunt explicabo. Nemo enim ipsam voluptatem quia voluptas sit aspernatur aut odit aut fugit, sed quia consequuntur magni dolores eos qui ratione voluptatem sequi nesciunt. Neque porro quisquam est, qui dolorem ipsum quia dolor sit amet, consectetur, adipisci velit, sed quia non numquam eius modi tempora incidunt ut labore et dolore magnam aliquam quaerat voluptatem. Ut enim ad minima veniam, quis nostrum exercitationem ullam corporis suscipit laboriosam, nisi ut aliquid ex ea commodi consequatur? Quis autem vel eum iure reprehenderit qui in ea voluptate velit esse quam nihil molestiae consequatur, vel illum qui dolorem eum fugiat quo voluptas nulla pariatur?
Sed ut perspiciatis unde omnis iste natus error sit voluptatem accusantium doloremque laudantium, totam rem aperiam, eaque ipsa quae ab illo inventore veritatis et quasi architecto beatae vitae dicta sunt explicabo. Nemo enim ipsam voluptatem quia voluptas sit aspernatur aut odit aut fugit, sed quia consequuntur magni dolores eos qui ratione voluptatem sequi nesciunt. Neque porro quisquam est, qui dolorem ipsum quia dolor sit amet, consectetur, adipisci velit, sed quia non numquam eius modi tempora incidunt ut labore et dolore magnam aliquam quaerat voluptatem. Ut enim ad minima veniam, quis nostrum exercitationem ullam corporis suscipit laboriosam, nisi ut aliquid ex ea commodi consequatur? Quis autem vel eum iure reprehenderit qui in ea voluptate velit esse quam nihil molestiae consequatur, vel illum qui dolorem eum fugiat quo voluptas nulla pariatur?
]]>Lorem Ipsum is simply dummy text of the printing and typesetting industry. Lorem Ipsum has been the industry’s standard dummy text ever since the 1500s, when an unknown printer took a galley of type and scrambled it to make a type specimen book. It has survived not only five centuries, but also the leap into electronic typesetting, remaining essentially unchanged. It was popularised in the 1960s with the release of Letraset sheets containing Lorem Ipsum passages, and more recently with desktop publishing software like Aldus PageMaker including versions of Lorem Ipsum.
Lorem Ipsum is simply dummy text of the printing and typesetting industry. Lorem Ipsum has been the industry’s standard dummy text ever since the 1500s, when an unknown printer took a galley of type and scrambled it to make a type specimen book. It has survived not only five centuries, but also the leap into electronic typesetting, remaining essentially unchanged. It was popularised in the 1960s with the release of Letraset sheets containing Lorem Ipsum passages, and more recently with desktop publishing software like Aldus PageMaker including versions of Lorem Ipsum.
Lorem Ipsum is simply dummy text of the printing and typesetting industry. Lorem Ipsum has been the industry’s standard dummy text ever since the 1500s, when an unknown printer took a galley of type and scrambled it to make a type specimen book. It has survived not only five centuries, but also the leap into electronic typesetting, remaining essentially unchanged. It was popularised in the 1960s with the release of Letraset sheets containing Lorem Ipsum passages, and more recently with desktop publishing software like Aldus PageMaker including versions of Lorem Ipsum.
]]>