--- layout: plugin title: E-ACSL description: Runtime Verification Tool key: main swipper: yes download: http://frama-c.com/download/e-acsl/e-acsl-manual-19.0-Potassium.pdf ---
Overview

Frama-C's E-ACSL plug-in automatically translates an annotated C program into another program that detects the violated annotations at runtime. If no annotation is violated, the behavior of the new program is the same as the one of the original program.

Combined with other Frama-C plug-ins that generate annotations, the verification process is pretty automatic and may verify much more properties than standard testing. This way, it is a memory debugger offering functionalities comparable to Valgrind or AddressSanitizer, and even more powerful.

Quick Start

E-ACSL comes with a convenient script e-acsl-gcc.sh which may be called as follow:

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

It generates three files ./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 instrumented file with the monitor generated by E-ACSL from the input files. The third one is the binary produced by gcc from this latter file, so monitoring the annotations. Its execution behaves in the same way than the two other files, except that it fails if an annotation is violated.

In order to automatically check that no undefined behaviors of many kinds are executed, just used it as follow:

	$ e-acsl-gcc.sh -c --rte=all <files>