Information Technology Reference
In-Depth Information
no dynamic check fails and the whole program does not fail with a runtime error
either. Therefore, a potential runtime error does not remain unnoticed thanks
to explicit annotations added by rte and checked by e-acsl.
Consider for instance the function
sum
of Fig. 3 in which we modify line 18
idx = i
*
size + j;
into the incorrect line
idx = i
*
size + j + 1;
. Since the index
idx
is now too great, that introduces an access out of the bounds of the matrices
a
,
b
,and
c
when computing the sum. We also complete this program with the
following test function.
1
int
main(
void
){
2
int
a[]={1,1,1,1}, b[]={2,2,2,2};
matrix c = sum(a, b, 2);
3
free(c);
4
return
0;
5
6
}
Running the rte plug-in on this program generates several additional annota-
tions corresponding to potential arithmetic overflows while computing
idx
or the
sum of the matrices' elements, and potential invalid memory accesses when read-
ing the matrices' elements. You can see them in the Frama-C GUI by running
the following command.
frama-c-gui -rte sum.c
Below are two examples of such annotations.
/
*
@
assert
rte: signed_overflow: i
*
size <= 2147483647;
*
/
/
*
@
assert
rte: mem_access:
\valid
(c+idx);
*
/
We can now combine the rte and e-acsl plug-ins to translate these additional
annotations (and the already existing ones) into C code in the following way.
frama-c sum.c -rte -machdep x86_64 -e-acsl-prepare -then -e-acsl
\
-then-on e-acsl -print -ocode out.c
The special option
-e-acsl-prepare
tells Frama-C to generate an e-acsl-compa-
tible abstract syntax tree (AST). It is required when the computation of the AST
is needed by another analysis than e-acsl (here by the generation of annotations
by rte).
Now, if we compile and run the resulting program
out.c
as shown in Fig. 4, we
get the following output which indicates that an assertion preventing a memory-
access error failed when dereferencing
c+idx
at line 19.
Assertion failed at line 19 in function sum.
The failing predicate is:
rte: mem_access:
\valid
(c+idx).
5.2 Verifying Annotations Statically
Frama-C comes with two static analyzers which try to verify acsl specifica-
tions: Value, based on abstract interpretation [15], and wp, based on weakest
precondition calculus [16].
