------
				README
				------

===============================================================================
				SUMMARY
===============================================================================

0) Summary
1) What Is
2) Simple usage
3) Examples
5) Compatibility with previous releases
6) Have Fun with E-ACSL!

===============================================================================
				WHAT IS
===============================================================================

This package contains the Frama-C's E-ACSL plug-in. It 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 the annotation is violated at runtime.

Annotations must be written in a subset of ACSL (ANSI/ISO C Specification
Language), namely E-ACSL (Executable ANSI/ISO C Specification Language). E-ACSL
is fully described in file doc/manuals/e-acsl.pdf.

This plug-in is still in a preliminary state: some parts of E-ACSL are not yet
implemented. What is supported is described in file
doc/manuals/e-acsl-implementation.pdf.

Please read file INSTALL for details about the installation procedure of
this plug-in and consult http://frama-c.com and http://frama-c.com/acsl
for information about Frama-C and ACSL.

The user manual is available at:
    http://frama-c.com/download/e-acsl/e-acsl-manual.pdf

===============================================================================
				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 only options is -c in order to compile the generated file which
contains the inline monitor from the input files. It 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
===============================================================================

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:

$ 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.

===============================================================================
			COMPATIBILITY WITH PREVIOUS RELEASES
===============================================================================

Changes are documented in a textual way in file Changelog.

===============================================================================
				HAVE FUN WITH E-ACSL!
===============================================================================