Information Technology Reference
In-Depth Information
-
to translate into C and evaluate memory-related e-acsl annotations; and
-
to record memory-related program operations in the store.
The following subsections present these two aspects in detail.
3.1 Translation and Evaluation of Memory-Related Annotations
When a specified property is violated at runtime, the instrumented code gener-
ated by e-acsl2c calls a special function, that we denote here
e_ascl_fail
,whose
default version reports the assertion failure and exits the execution.
1
The instrumentation is different for an internal annotation in a function and
for a function contract. An annotation inside a function
f
is directly translated
by e-acsl2c into C code that checks the annotation condition inside
f
(this case
will be illustrated on Fig. 7). For a function
f
with a function contract, e-acsl2c
adds a new C function
__e_acsl_f
with the same signature as
f
, and replaces all
initial calls to
f
by calls to
__e_acsl_f
. Basically,
__e_acsl_f
contains three parts:
checking the precondition of
f
,acallto
f
and checking the postcondition of
f
.
Thus a contract of
f
is systematically checked by
__e_acsl_f
in the instrumented
code whenever
f
is called in the original code, even if the code of
f
is not provided
during the instrumentation step.
The library provides primitives for the most frequently used memory-related
e-acsl annotations shown in Fig. 1. They have the same role and similar names
(with “
__
”asprefixinsteadof“
\
”). For the last three of them, library func-
tions expect an additional second argument indicating the size (in bytes) of the
memory location
*
p
.
For example, Fig. 3 presents (a simplified version of) function
__e_acsl_findchr
automatically generated by e-acsl2c for the function
findchr
of Fig. 2. Lines 4-5
of Fig. 3 check the precondition (and report any violation). Lines 6-9 compute
if the first behavior's
assumes
clause is satisfied, i.e. if this behavior is applicable
for the current call of
findchr
. Since execution of an e-acsl annotation must not
introduce any risk of runtime error, an additional check of validity of reading
s[i]
is automatically added at line 7 before an access to
s[i]
. Similarly, lines
10-13 compute if the second behavior is activated by the current call of
findchr
.
Then
findchr
is called line 14. Next, lines 15-22 check that if the first behavior's
assumption is true, its postconditions are satisfied as well. Again, to avoid any
risk of a runtime error inserted by e-acsl2c, an additional validity check is
added at line 20 before an access to
*
__res
. Similarly, the second behavior is
checked at lines 23-25.
3.2 Recording Validity and Initialization Data in the Store
In order to be able to provide requested information on memory locations, the
code instrumented by e-acsl2c records in the store for each block the
block
1
Actual instrumentation allows the user to customize this function by defining its
own action according to several parameters [7].
