Information Technology Reference
In-Depth Information
1
#include
"sum.c"
2
extern
size_t __memory_size;
3
4
matrix sum3(matrix a, matrix b, matrix c,
int
size) {
5
matrix x, y;
x = sum(a, b, size);
6
y = sum(x, c, size);
7
return
y;
8
9
}
10
11
void
main(
void
){
12
int
a[] = {1,1,1,1}, b[] = {2,2,2,2}, c[] = {3,3,3,3};
matrix d;
13
L1: d = sum3(a, b, c, 2);
14
L2: free(d);
15
//@
assert \at
(__memory_size,L2) -
\at
(__memory_size,L1) <=
sizeof
(
int
)
*
4;
16
17
}
Fig. 5.
Function
sum3
returns the sum of three given square matrices of given size
so the user may investigate this difference between two closer points, replacing
the assertion at line 16 by another one:
//@
assert \at
(__memory_size,L2)-
\at
(__memory_size,L1) <=
sizeof
(
int
)
*
size
*
size;
indicating that only an array of
size
*
size
integers can be allocated between
L1
and
L2
. This assertion fails again, indicating that the memory leak probably
happens inside the function
sum3
. Inserting a postcondition of function
sum3
at
line 3
//@
ensures
__memory_size -
\old
(__memory_size) ==
sizeof
(
int
)
*
size
*
size;
precisely comparing the size of dynamically allocated memory before and after
the function call is another way to find out that the memory leak occurs in
function
sum3
. The problem is indeed due to the allocation for the array returned
at line 6 of Fig. 5 that becomes inaddressable when function
sum3
exits. To solve
this issue,
free(x);
should be inserted before the
return
statement at line 8 of
Fig. 5.
4 Runtime Checking and Analysis of Proof Failures
As we have shown in the previous section, runtime assertion checking helps to
ensure that the program execution respects the provided annotations. When the
annotations are supposed to be correct, an annotation failure reveals an error in
the program. But runtime assertion checking can be also used in a dual way, to
find a potentially incorrect annotation. It can also provide more confidence in
conformance of the program to its specification when no failures are detected.
This approach can be very helpful during proof of programs.
Indeed, in order to formally prove a program, the validation engineer has to
specify it. This is a tedious task, and errors in the first versions of specifications
are very common. Moreover, when the program proof fails, the proof failure is
not necessarily due to a wrong specification or a wrong implementation, but can
