E-ACSL
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 and AddressSanitizer, and even more powerful.
More precisely, possible usages include:
- detection of a large class of undefined behaviors (in conjunction with the RTE plug-in);
- verification of high-level properties (in conjunction for instance with the Aoraï or SecureFlow plug-ins);
- complementing static and dynamic analyses (i.e. trying to find test cases that trigger alarms generated by Eva or act as counter-examples for annotations marked as unknown by WP), in conjunction with the StaDy plug-in;
- debugging specifications, in conjunction with a test-case generator such as PathCrawler or AFL
Quick Start
E-ACSL comes with a convenient script e-acsl-gcc.sh which may be called as follows:
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 as 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, the script can be simply used as follows:
e-acsl-gcc.sh -c --rte=all <files>Dependencies
The E-ACSL plug-in can use the results of both RTE and Eva plug-ins. It can be combined with several other plug-ins, such as WP, Aoraï, SecureFlow, StaDy, PathCrawler, MetACSL, etc.