Newer
Older
Andre Maroneze
committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
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
72
73
---
layout: plugin
title: E-ACSL
description: Runtime Verification Tool
key: main
manual_pdf: http://frama-c.com/download/e-acsl/e-acsl-manual.pdf
extra_manual_name: E-ACSL Language Reference Manual
extra_manual_pdf: http://frama-c.com/download/e-acsl/e-acsl.pdf
third_manual_name: E-ACSL Language Reference Implementation Manual
third_manual_pdf: http://frama-c.com/download/e-acsl/e-acsl-implementation.pdf
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), etc.
## Further Reading
- [E-ACSL User Manual]({{page.manual_pdf}})
- [{{page.extra_manual_name}}]({{page.extra_manual_pdf}})
- [{{page.third_manual_name}}]({{page.third_manual_pdf}})