Information Technology Reference
In-Depth Information
#!/bin/sh
share='frama-c -print-share-path'
frama-c -pp-annot -machdep x86_64 $1 -e-acsl -then-on e-acsl -print -ocode out.c
gcc -DE_ACSL_MACHDEP=x86_64 out.c $share/e-acsl/e_acsl.c
$share/e-acsl/memory_model/e_acsl_bittree.c
$share/e-acsl/memory_model/e_acsl_mmodel.c -o runme -lgmp
./runme
Fig. 4.
Script
check.sh
that instruments the file given in its argument with e-acsl
plug-in, compiles and executes it
tions and postconditions, function calls in a context that does not respect the
callee's precondition, potential segmentation faults and memory leaks.
3.1
e-acsl
Plug-In and Assertion Failures
We assume that the Frama-C platform with e-acsl plug-in
2
and the
gcc
compiler have been installed on the machine. Suppose the file
absval.c
con-
tains the program of Fig. 1b. This program can be instrumented with the
e-acsl plug-in, compiled and executed on a Linux machine by the command
./check.sh absval.c
using the script given at Fig. 4. The options
-machdep x86_64
and
-DE_ACSL_MACHDEP=x86_64
should be used for a 64-bit machine (a 32-bit archi-
tecture
x86_32
is currently assumed by default).
The instrumentation translates the e-acsl specification into executable C
code that performs corresponding runtime checks and reports any failure. For
Fig. 1b, two assertions at lines 9 and 11 will be checked at runtime exactly as for
Fig. 1a. The first one is verified (producing no output), while the second one fails
due to a wrong inequality at line 3. The program exits with an explicit message:
Assertion failed at line 11 in function main. The failing predicate is: n == 3.
Section 6 shows how the user can customize the actions when checking the
validity of a predicate.
3.2 Function Contracts
Providing function contracts makes runtime assertion checking even more sys-
tematic and powerful. When a function is specified with an e-acsl contract
(with a pre- and/or a postcondition), the e-acsl plug-in performs their system-
atic checks on entry (for the precondition) and on exit (for the postcondition)
each time the function is called. Suppose we complete the file of Fig. 2a (or
Fig. 2b) with a simple function
1
int
main(){
2
absval(0);
absval(3);
3
absval(INT_MIN);
4
return
0;
5
6
}
