Information Technology Reference
In-Depth Information
Runtime checking with the e-acsl plug-in for this example reports a postcon-
dition failure at line 9 of Fig. 3 since the elements of
c
are not valid after exiting
the function
sum
. Thanks to the postcondition, e-acsl prevents invalid accesses
to the elements
c[0]
and
c[2]
in function
main
.Thisisanexampleofa
temporal
error
, i.e. an invalid memory access to a deallocated memory object.
Another example of a temporal error is a use-after-free. To give an example,
we complete the program of Fig. 3 with the 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
//@
assert \valid
(&c[0]) &&
\valid
(&c[2]);
5
int
trace = c[0] + c[2];
6
return
0;
7
8
}
Runtime checking with the e-acsl plug-in for this example reports an assertion
failure since the accesses to
c[0]
and
c[2]
in function
main
become invalid after
the array is freed.
Notice that memory access validity is only checked when it is specified by
(or required for safe translation of) the provided e-acsl annotations. We show
in Section 5 how to enforce memory safety checks with the e-acsl plug-in by
automatic generation of annotation using the rte plug-in.
3.4 Memory Leaks
Memory leaks represent another common type of defects in programs with inten-
sive dynamic memory allocation. A
memory leak
appears when an inaddressable
memory object remains uselessly stored on the system reducing the amount of
available memory. In some cases, memory leaks can be a serious problem for pro-
grams running for a long time and/or containing frequent memory allocations.
When the amount of available memory decreases, the developer may suspect
memory leaks. In this case it can be helpful to define (or to bound) the expected
difference of the size of dynamically allocated memory at two program points. If
the amount of allocated memory increases unexpectedly, additional annotations
specifying the difference between closer and closer points may help to find the
precise function where the memory leak occurs. The e-acsl plug-in provides
such a means to precisely control the amount of dynamically allocated memory
that helps to detect memory leaks.
To illustrate this feature, consider the program of Fig. 5. It includes the file
sum.c
of Fig. 3 and defines a function
sum3
computing the sum of three given
matrices. If the program performs frequent calls to such a function
sum3
,the
amount of available memory will decrease. The size of dynamically allocated
memory in bytes can be referred by the variable
__memory_size
(line 2 of Fig. 5)
defined by the memory monitoring library of the e-acsl plug-in. Line 16 of
function
main
illustrates how the user can specify that the amount of dynamically
allocated memory must not change between two points, at label
L1
before the call
to
sum3
and at line 16 after deallocating the returned array
d
. This assertion fails,
