E-ACSL plug-in

Try it now!
source tarball of the plug-in
Reference Manual
executable subset of ACSL
Implementation Status
what is still not yet implemented The Frama-C's E-ACSL plug-in takes as input an annotated C program and returns the same program in which annotations have been converted into C code dedicated to runtime assertion checking: this code fails at runtime if and only if the annotation is violated at runtime.

Annotations must be written in a subset of ACSL, namely E-ACSL (Executable ANSI/ISO C Specification Language).

This plug-in is still in a preliminary state: some parts of E-ACSL are not yet implemented.

Simple Usage

The standard use is the following:

$ frama-c -e-acsl <files> -then-on e-acsl -print -ocode generated_code.c

Option -e-acsl runs the Frama-C's E-ACSL plug-in on the given <files>: it computes a new Frama-C project called `e-acsl'. Option -then-on switches to this project while options -print and -ocode pretty prints the corresponding C code into file `generated_code'.

Here the only E-ACSL specific option is -e-acsl. The others (-then-on, -print and -ocode) are standard Frama-C options, described in the Frama-C User Manual as well as the concept of Frama-C Project.

The generated file is a C file which usually depends on the GMP library. The following commands compile and run it:

$ gcc generated_code.c -lgmp -o generated_code
$ ./generated_code

The execution behaves in the same way than the original <files>, except that it fails if an annotation is violated.

Examples

1. Consider the following C program:

   // true.i
   int main(void) {
     /*@ assert \true; */
     return 0;
   }
   

   Since the assertion is always true, the generated code behaves in the same way that just returning 0:

   $ frama-c -e-acsl true.i -then-on e-acsl -print -ocode gen_true.c
   $ gcc gen_true.c -o gen_true
   $ ./gen_true
   $ echo $?
   0
   

   As this example is trivial, the generated code does not require to be linked against GMP. It is usually not the case.
2. Now consider the following C program:

   // false.i
   int main(void) {
     int x = 0;
     /*@ assert x+1 == 0; */
     return 0;
   }
   

   Since the assertion is always false, the generated code fails at runtime:

   $ frama-c -e-acsl false.i -then-on e-acsl -print -ocode gen_false.c
   $ gcc gen_false.c -lgmp -o gen_false
   $ ./gen_false
   Assertion failed at line 7.
   The failing predicate is:
   (x+1 == 0).
   $ echo $?
   1
   

   As this example uses arithmetic in annotations, the generated code must be linked against GMP (GCC's option -lgmp) to be able to produce an executable.
3. More advanced examples are available in plug-in directory tests/e-acsl-runtime. Note that these examples never fail at runtime: all the annotations are valid.

Advanced usage

This E-ACSL plug-in is fully integrated within Frama-C: any standard Frama-C options may be used in order to customize the Frama-C execution. Read the Frama-C User Manual for additional information.

The list of E-ACSL option is available through the option -e-acsl-help:

$ frama-c -e-acsl-help

Main options are: