Information Technology Reference
In-Depth Information
1
frama-c -machdep x86_64 -e-acsl-prepare -val sum.c -then -e-acsl
\
2
-then-on e-acsl -print -ocode out.c
Linking and executing the generated program in the usual way does not report
any failure on this correct program.
6 Customization of Runtime Monitoring
By default, as shown in the previous examples, when the evaluation of a predicate
fails at runtime, the execution stops with an error message and exit code 1. This
behavior is implemented by the function
e_acsl_assert
provided in the file
e_acsl.c
of the e-acsl library. This function is called each time an annotation is checked.
It is fully possible to modify this behavior by providing your own definition of
e_acsl_assert
. The prototype of the function to implement is as follows.
void
e_acsl_assert(
int
,
char
*
,
char
*
,
char
*
,
int
);
For each annotation
a
to be checked, the parameters are the following:
-
the first one is the validity status of
a
(0 if false, non-zero if true);
-
the second one is a string describing the kind of
a
(an assertion, a precondi-
tion, a postcondition, etc);
-
the third one is the function name where
a
takes place;
-
the fourth one is a textual description of
a
;
-
the fifth one is the line number of
a
in the source file.
For instance, Fig. 6 provides an implementation which does not stop the program
execution, but appends an error message at the end of file
log_file.log
when an
annotation is violated.
Then, in the script of Fig. 4, we can replace the file
$share/e-acsl.c
by the one
defining the function of Fig. 6. Thus, executing it on the binary generated from
the first example of Section 3.3 generates a file
log_file.log
which contains the
following lines:
Precondition failed at line 8 in function sum.
The failing predicate is:
\forall integer
i,
integer
j;
(0 <= i && i < size) && (0 <= j && j < size) ==>
\valid
((b+i
*
size)+j).
RTE failed at line 11 in function sum.
The failing predicate is:
mem_access:
\valid_read
(__e_acsl_at_7
+(
long long
)((
long long
)((
long long
)__e_acsl_i_4
*
(
long long
)__e_acsl_at_8)
+(
long long
)__e_acsl_j_4)).
It indicates that there were actually two failed runtime checks. The former
was previously described in Section 3.3 and corresponds to the invalid precondi-
tion about the array
b
(which has 3 elements while 4 are expected). The latter
corresponds to an out-of-bound error detected when trying to evaluate the post-
condition since
b[i
*
size+j]
tries to access the fourth element of the array
b
of
length 3 (when
i
=1,
j
=1and
size
=2).
