Information Technology Reference
In-Depth Information
a)
b)
1
#include
<assert.h>
2
int
absval(
int
x){
3
1
// returns absolute value of x
2
int
absval(
int
x){
3
return
(x<0)?x:(-x);
return
(x<0)?x:(-x);
4
}
5
6
void
main(){
7
4
}
5
6
void
main(){
7
int
n;
int
n;
n=absval(0);
// test 1
n=absval(0);
// test 1
8
8
assert
(n==0);
//@
assert
n==0;
9
9
n=absval(3);
// test 2
n=absval(3);
// test 2
10
10
assert
(n==3);
//@
assert
n==3;
11
11
// other tests...
// other tests...
12
12
13
}
13
}
Fig. 1.
Function
absval
,specified
a)
with
assert
macros,
b)
with e-acsl assertions
translated into C, compiled and used as executable specification. An automatic
translator into C has been implemented in the e-acsl plug-in [7] of Frama-C.
This paper is organized as follows. Section 2 presents the executable specifi-
cation language e-acsl and illustrates how the e-acsl plug-in can be used to
automatically translate the specified C code into an instrumented version suit-
able for runtime verification of specified properties. Section 3 shows how this
solution can be used to automatically detect and report various kinds of errors
such as wrong assertions, wrong postconditions, function calls in a wrong context
(unsatisfied precondition) and memory leaks. The benefits of combining runtime
assertion checking with proof of programs are discussed in Section 4. Section 5
illustrates how existing Frama-C analyzers can make runtime assertion check-
ing even more ecient. On the one hand, automatic generation of assertions
for frequent runtime errors may help to thoroughly check the program for these
kinds of errors without manually writing assertions. On the other hand, some
assertions may be statically validated by a static analysis tool, reducing the
number of assertions to be checked. Section 6 shows how program monitoring
with e-acsl can be customized in order to define particular actions to be exe-
cuted whenever a failure is detected. Finally, Section 7 concludes the paper and
presents future work.
2 Executable Specifications in
e-acsl
Variouswaysofspecifyingassertionshave been proposed in the literature [1].
One of the simplest ways to insert an assertion into a C program and to check
it at runtime is to use the
assert
macro. Unless assertion checks are switched
off (usually, by setting the preprocessor option
NDEBUG
), the condition specified
as the argument of the
assert
macro is evaluated and whenever it is false, the
execution stops and the failure is reported. Fig. 1a illustrates this approach for
the function
absval
returning the absolute value of its argument, that is tested
by the function
main
. The code contains an error (wrong inequality at line 3)
that would be reported by the second assertion check (line 11).
