A Lesson on Runtime Assertion Checking with Frama-C - Runtime Verification - page 396

Consider again the function sum of Fig. 3 with the following test 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

return 0;

5

6 }

Combination with wp Plug-In. Running wp on this program (with the au-
tomatic theorem prover Alt-Ergo [17]) automatically proves the preconditions
of function sum as you can see, for instance, running the Frama-C GUI:
frama-c-gui -wp sum.c
It does not prove, however, the postconditions of the function: such a proof with
wp requires to write loop invariants for both loops of the function. Nevertheless
it is possible to combine wp and e-acsl: wp proves the preconditions 3 , while
e-acsl establishes that the postconditions are not violated for a given execution.
By default, the e-acsl plug-in does not perform code instrumentation to check
already proved properties: if wp proves the preconditions first, the code gener-
ated by e-acsl performs fewer runtime checks and so is more ecient. Such a
combination is run by the following command.
frama-c -machdep x86_64 -e-acsl-prepare -wp sum.c -then -e-acsl \
-then-on e-acsl -print -ocode out.c
The generated program out.c is then linked and executed as usual. In this par-
ticular case, it does not report any error since the program is actually correct.

Combination with Value Plug-In. We can run Value on the same example
as follows.
frama-c -val sum.c
Below is a summary of the output.
1 sum.c:6:[value] Function sum: precondition got status valid.
2 sum.c:7:[value] Function sum: precondition got status unknown.
3 sum.c:8:[value] Function sum: precondition got status unknown.
4 sum.c:19:[kernel] warning: out of bounds write. assert \valid (c+idx);
5 sum.c:9:[value] Function sum: postcondition got status unknown.
6 sum.c:10:[value] Function sum: postcondition got status unknown.
It indicates than Value automatically proves the first precondition size >= 1 ,
but does not prove neither the other ones 4 nor the postconditions. Value also
generates an acsl annotation because it detects a potential out-of-bounds access
when writing into the array cell c[idx] at address c+idx . It does not detect similar
out-of-bounds accesses for reading a[idx] and b[idx] because it assumes that the
preconditions of the function are valid.
In the same way as for wp, we can combine Value and e-acsl to dynamically
check with e-acsl only what remains unproved by Value. e-acsl will also check
the additional annotation generated by Value. Such a combination is run by
the following command.

3 The wp's default memory model assumes that malloc never returns NULL .
4 The Va lue's default memory model assumes that malloc may return NULL .