Information Technology Reference
In-Depth Information
1
#include
<stdio.h>
2
3
void
e_acsl_assert
4
(
int predicate
,
char
*
kind,
char
*
fct,
char
*
pred_txt,
int
line)
5
{
6
if
(!
predicate
){
7
FILE
*
f = fopen("log_file.log", "a");
8
fprintf(f,
9
"%s failed at line %d in function %s.
\n\
10
The failing predicate is:
\n
%s.
\n
",
11
kind, line, fct, pred_txt);
fclose(f);
12
}
13
14
}
Fig. 6.
Modifying the runtime behavior when an annotation is violated
7 Conclusion and Future Work
In this tutorial paper, we have presented how the e-acsl plug-in of Frama-C
can be used to perform runtime assertion checking of C programs. The user
expresses the expected properties of the program statements and functions in a
powerful formal specification language. These properties are then automatically
translated into C code in order to be checked at runtime.
In addition to usual runtime assertion checking, e-acsl may help to debug
specifications before proving a program formally. When combined with other
Frama-C analyzers, e-acsl is even more ecient: it may automatically check
for any runtime errors in C programs, and may discard runtime checks of prop-
erties previously statically verified.
Future work includes the support of missing parts of the e-acsl specification
language, in particular assigns clauses, loop invariants and variants, and logic
functions and predicates. It also includes the verification of new kinds of prop-
erties like additional memory temporal properties, LTL properties or security
properties, and new areas of application like combinations of testing and static
analysis, security monitoring and teaching formal specification.
References
1. Clarke, L.A., Rosenblum, D.S.: A historical perspective on runtime assertion check-
ing in software development. ACM SIGSOFT Software Engineering Notes 31(3),
25-37 (2006)
2. Correnson, L., Cuoq, P., Kirchner, F., Prevosto, V., Puccetti, A., Signoles, J.,
Yakobowski, B.: Frama-C User Manual (April 2013),
http://frama-c.com
3. Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.:
Frama-C, a program analysis perspective. In: Eleftherakis, G., Hinchey, M., Hol-
combe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233-247. Springer, Heidelberg
(2012)
4. Baudin, P., Filliatre, J.C., Hubert, T., Marche, C., Monate, B., Moy, Y., Prevosto,
V.: ACSL: ANSI/ISO C Specification Language, v1.6. (April 2013),
