Information Technology Reference
In-Depth Information
1
char
*
__e_acsl_findchr(
char
*
s,
char
c,
unsigned int
n) {
2
char
*
__res;
unsigned int
i;
int
__e_acsl_exists = 0;
int
__e_acsl_forall = 1;
3
if
(!( __valid_read(s,1) && __offset(s)+n <= __block_length(s) ))
4
e_acsl_fail("findchr","Pre","line 3");
5
for
( i=0; i<n && __e_acsl_exists == 0 ; i++ ) {
6
if
(! __valid_read(s+i,1)) e_acsl_fail("findchr","mem_access:s[i]","line 5");
7
if
( s[i] == c ) __e_acsl_exists = 1;
8
}
9
for
( i=0; i<n && __e_acsl_forall == 1 ; i++ ) {
10
if
(! __valid_read(s+i,1)) e_acsl_fail("findchr","mem_access:s[i]","line 10");
11
if
(!( s[i] != c )) __e_acsl_forall = 0;
12
}
13
__res = findchr(s, c, n);
14
if
( __e_acsl_exists ){
15
if
(!( __base_addr(s) == __base_addr(__res) ))
16
e_acsl_fail("findchr","Post","line 6");
17
if
(!( __offset(s) <= __offset(__res) && __offset(__res) < __offset(s)+n ))
18
e_acsl_fail("findchr","Post","line 7");
19
if
(! __valid_read(__res,1)) e_acsl_fail("Post","mem_access:
*
__res","line 8");
20
if
(!(
*
__res == c )) e_acsl_fail("Post","findchr","line 8");
21
}
22
if
( __e_acsl_forall )
23
if
(!( __res == (
void
*
)0 )) e_acsl_fail("Post","findchr","line 11");
24
return
__res;
25
26
}
Fig. 3.
Simplified version of function
__e_acsl_findchr
automatically generated by
e-acsl2c for runtime checking of the contract for the function
findchr
of Fig. 2
Function Its meaning
__store_block(p,len)
records a block of size
len
and base address
p
in the store
__delete_block(p)
removes existing block with base address
p
from the store
__malloc(len)
allocates a block of size
len
and records it in the store
__free(p)
deallocates the block with base
p
and removes it from the store
__initialize(p,len)
marks
len
bytes starting from pointer
p
as initialized
__full_init(p)
marks the whole block with base address
p
as initialized
Fig. 4.
Basic recording primitives provided by the memory monitoring library
metadata
including its base address, size (in bytes), validity status (whether
reading or writing the block is safe) and the initialization status for each byte of
the block. Our memory monitoring library has been designed to be compatible
with various implementations of the underlying store. This section presents the
instrumentation scheme for recording operations using high-level library prim-
itives, while the store implementation and optimizations are discussed later in
Sec. 4, 5 and 6.
Fig. 4 presents some recording primitives provided by the library. They allow
to register a new block in the store, to mark some particular bytes (or the
whole block) as initialized and to remove the block from the store when it is
not valid anymore. For convenience, instrumented versions of basic dynamic
allocation functions (
malloc
,
calloc
,
realloc
,
free
) are provided as well. They
directly add/remove from the store the allocated/deallocated block (and, in case
of
realloc
, transfer recorded initialization information for the old block to the
new one).
