E-ACSL plug-in

Try it now!
source tarball of the plug-in
User Manual
how to use the plug-in
Reference Manual
what is the specification language
Implementation Status
what is still not yet implemented
Frama-C's E-ACSL plug-in automatically translates an annotated C program into another program that fails at runtime if an annotation is violated. If no annotation is violated, the behavior of the new program is exactly the same as the one of the original program.

Annotations must be written in the E-ACSL specification language, which is a subset of ACSL. This plug-in is still in a preliminary state: some parts of E-ACSL are not yet supported.

Simple Usage

E-ACSL comes with a convenient script e-acsl-gcc.sh. The standard use is the following:

$ e-acsl-gcc.sh -c <files>

Here the option -c compiles the generated file which contains the inline monitor from the input files. The command outputs three binaries ./a.out, ./a.out.frama-c and ./a.out.e-acsl. The first one is the binary produced by gcc from the input files, the second one is the binary produced by gcc with the file generated by Frama-C from the input files, but without monitoring any annotation. The third one is the binary produced by gcc with the file generated by Frama-C from the input files, and monitoring the annotations. Its execution behaves in the same way than the two other files, except that it fails if an annotation is violated.

Please refer to the user manual for details about e-acsl-gcc.sh.

Examples

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:

$ e-acsl-gcc.sh -c true.i
$ ./a.out.e-acsl
$ echo $?
0

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:

$ e-acsl-gcc.sh -c false.i
$ ./a.out.e-acsl
Assertion failed at line 4.
The failing predicate is:
x + 1 == 0.
$ echo $?
1

More advanced examples are available in the user manual and in the plug-in directory tests/e-acsl-runtime.