------
				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
===============================================================================

The standard use is the following:

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

Option -e-acsl runs the Frama-C's E-ACSL plug-in on the given <files>: it
generates a new Frama-C project. Option -then-last 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 standard C file.
In simple cases, the following commands compile and run it:

$ gcc `frama-c -print-share-path`/e-acsl/e_acsl.c generated_code.c -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.

In more complex cases, additional files must also be linked.
See the user manual for details.

===============================================================================
				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-last -print -ocode gen_true.i
$ gcc `frama-c -print-share-path`/e-acsl/e_acsl.c gen_true.i -o gen_true
$ ./gen_true
$ echo $?
0

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-last -print -ocode gen_false.i
$ gcc `frama-c -print-share-path`/e-acsl/e_acsl.c gen_false.i -o gen_false
$ ./gen_false
Assertion failed at line 3.
The failing predicate is:
x+1 == 0.
$ echo $?
1

3) More advanced examples are available in the user manual and in the directory
   tests/runtime.

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

Changes are documented in a textual way in file Changelog.

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