Newer
Older
Andre Maroneze
committed
---
layout: plugin
title: E-ACSL
description: Runtime Verification Tool
key: main
manual_pdf: /download/e-acsl/e-acsl-manual.pdf
- name: "E-ACSL language reference manual"
short: "Language reference"
link: /download/e-acsl/e-acsl.pdf
- name: "E-ACSL language reference implementation manual"
name_for_main_dl: "E-ACSL implementation"
link: /download/e-acsl/e-acsl-implementation.pdf
Andre Maroneze
committed
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
distrib_mode: main
---
## 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](https://en.wikipedia.org/wiki/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](rte.html) plug-in);
- verification of high-level properties (in conjunction for
instance with the [Aoraï](aorai.html) or [SecureFlow](secureflow.html)
plug-ins);
- complementing static and dynamic analyses (i.e. trying to
find test cases that trigger alarms generated by [Eva](eva.html) or act
as counter-examples for annotations marked as unknown by [WP](wp.html)),
in conjunction with the [StaDy](stady.html) plug-in;
- debugging specifications, in conjunction with a test-case generator such as
[PathCrawler](pathcrawler.html) or [AFL](http://lcamtuf.coredump.cx/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](rte.html) and
[Eva](eva.html) plug-ins. It can be combined with several other plug-ins,
such as [WP](wp.html), [Aoraï](aorai.html), [SecureFlow](secureflow.html),
[StaDy](stady.html), [PathCrawler](pathcrawler.html), [MetACSL](metacsl.html), etc.
Andre Maroneze
committed
## Further Reading
{% for add in page.additional %}
- [{{add.name}}]({{add.link}}){% endfor %}