Information Technology Reference
In-Depth Information
1
/
*
@
requires \valid_read
(s) &&
\offset
(s)+n <=
\block_length
(s);
2
@
behavior
found:
@
assumes \exists int
i;0<=i<n&&s[i] == c;
3
@
ensures \base_addr
(s) ==
\base_addr
(
\result
);
4
@
ensures \offset
(s) <=
\offset
(
\result
)<
\offset
(s)+n;
5
@
ensures
*
\result
== c;
6
@
behavior
not_found:
7
@
assumes \forall int
i; 0 <= i < n ==> s[i] != c;
8
@
ensures \result
==
\null
;
9
10
@
*
/
11
char
*
findchr(
char
*
s,
char
c,
unsigned int
n) {
12
unsigned int
i;
for
(i = 0; i < n; i++)
13
if
(s[i] == c)
14
return
s+i; // found, returns the pointer
15
return
(
void
*
)0; // not found, returns NULL
16
17
}
Fig. 2.
Function
findchr
specified with an e-acsl contract
value (keyword
\result
) must refer to the same block as
s
(line 4), to one of the
n
characters starting from
*
s
(line 5), and the referred character must be equal
to
c
(line 6). Similarly, the second behavior states that the null pointer must be
returned (line 9) whenever
c
in not present in the array (line 8).
Translation into C of basic e-acsl features (including overflow-free arithmetic
operations for integers, behaviors, quantifications over finite sets, some special
keywords, values at the Pre, Post or any labeled state, etc.) was described in [6].
However, runtime assertion checking of e-acsl specifications involving memory-
related constructs of Fig. 1 is particularly complex. Languages with pointers,
such as C or C++, do not allow the developer to easily check for pointer va-
lidity. The developer is supposed to know when a pointer is valid or not. For
example, even when the size of an input array
a
is provided in a function sig-
nature
int
f(
int
a[10])
, it is ignored according to the ISO C 99 norm [15, Sec.
6.7.5.3.7]. In other words, this declaration is equivalent to
int
f(
int
*
a)
,sothe
array size is lost. At runtime,
sizeof
(a)
inside
f
returns the size of a pointer, and
nothing guarantees that
a
really refers to an array with 10 elements. Runtime
checking of memory-related e-acsl annotations can be realized using systematic
monitoring of memory operations as shown in the next section.
3 Memory Monitoring for
e-acsl
: An Overview
Runtime assertion checking of e-acsl specifications is based on a non-invasive
source code instrumentation by e-acsl2c. In order to evaluate memory-related
e-acsl annotations (Fig. 1), we record information on validity and initializa-
tion of memory locations during program execution in a dedicated data store,
that we call below
the store.
We have developed a memory monitoring library
that provides primitives for both evaluating memory-related e-acsl annotations
(by making queries to the store) and recording in the store all necessary data
on allocation, deallocation and initialization of memory blocks. Thus e-acsl2c
inserts calls to library primitives for two purposes:
