Frama-C http://localhost:8000 Mon, 28 May 2018 13:01:21 +0000 en-US hourly 1 https://wordpress.org/?v=4.8 Frama-C 15 (Phosphorus) released, and open source case studies http://localhost:8000/sample-blog-1/ http://localhost:8000/sample-blog-1/#respond Fri, 01 Sep 2017 12:00:56 +0000 https://framac-staging.eu-staging.kacdn.net/?p=495 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.

]]>
http://localhost:8000/sample-blog-1/feed/ 0
Sample Blog Content http://localhost:8000/sample-blog-content/ http://localhost:8000/sample-blog-content/#respond Fri, 11 Aug 2017 12:57:08 +0000 https://framac-staging.eu-staging.kacdn.net/?p=440 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?

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?

]]>
http://localhost:8000/sample-blog-content/feed/ 0
Content http://localhost:8000/content/ http://localhost:8000/content/#respond Fri, 04 Aug 2017 06:16:35 +0000 http://frama-c.com/?p=312 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.
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.

]]>
http://localhost:8000/content/feed/ 0
Dummy http://localhost:8000/dummy/ http://localhost:8000/dummy/#respond Fri, 04 Aug 2017 06:16:29 +0000 http://frama-c.com/?p=310 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.
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.

]]>
http://localhost:8000/dummy/feed/ 0
Ipsmu http://localhost:8000/ipsmu/ http://localhost:8000/ipsmu/#respond Fri, 04 Aug 2017 06:16:22 +0000 http://frama-c.com/?p=308 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.
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.

]]>
http://localhost:8000/ipsmu/feed/ 0
Lorem http://localhost:8000/lorem/ http://localhost:8000/lorem/#respond Fri, 04 Aug 2017 06:16:15 +0000 http://frama-c.com/?p=306 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.
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.

]]>
http://localhost:8000/lorem/feed/ 0
Desc http://localhost:8000/desc/ http://localhost:8000/desc/#respond Fri, 04 Aug 2017 06:16:05 +0000 http://frama-c.com/?p=304 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.
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.

]]>
http://localhost:8000/desc/feed/ 0
Demo http://localhost:8000/demo/ http://localhost:8000/demo/#respond Fri, 04 Aug 2017 06:15:34 +0000 http://frama-c.com/?p=302 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.

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.

]]>
http://localhost:8000/demo/feed/ 0
test http://localhost:8000/test/ http://localhost:8000/test/#respond Thu, 03 Aug 2017 09:36:16 +0000 http://frama-c.com/?p=285 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.
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.

]]>
http://localhost:8000/test/feed/ 0