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

and instrument and run it using the script of Fig. 4. For each call of absval ,the
precondition is checked before the call and the postcondition is checked after the
call without requiring any additional assertions. The checks for the first two calls
succeed, while the call absval(INT_MIN) violates the precondition, so the program
exits and reports:

Precondition failed at line 2 in function absval.
The failing predicate is: x > -2147483647-1.

If the inequality at line 8 of Fig. 2a was erroneously written again as “ < ”,
the program would exit after the call absval(3) and explicitly report a postcon-
dition failure. In this way, the preconditions and postconditions are automati-
cally ensured by the instrumented code for each function call. In particular, the
precondition check guarantees that the function is called on admissible inputs
and prevents from calling it in an inappropriate context. The current release of
e-acsl does not yet support runtime checking of the assigns clause, this feature
will be integrated in a future version.

3.3 Segmentation Faults

Segmentation faults represent one of the most important issues in C programs.
Some of them may lead to runtime errors, others may remain unnoticed and
provoke memory corruption. To address this issue, the e-acsl plug-in provides
a memory monitoring library [13] and allows the user to check specified memory-
related properties at runtime. Let us illustrate this feature on the program of
Fig. 3 completed with the following test function.
1 int main( void ){
2

int a[]={1,1,1,1}, b[]={2,2,2}; // one element missing, should be {2,2,2,2}

matrix c = sum(a, b, 2); 3

free(c); 4

return 0; 5

6 }

The resulting file can be instrumented by the e-acsl plug-in and run using the
script of Fig. 4. The execution reports a failure in the precondition of sum at line
8 of Fig. 3 since the array b has 3 elements instead of 4 as expected for a 2

×

2
matrix. Thanks to the precondition, e-acsl prevents an invalid access to b[3]
at line 18 of Fig. 3 that would be out-of-bounds. This is an example of a spatial
error , i.e. an invalid memory access due to an out-of-bounds offset or array index.
To correct this error, the array b must be initialized with 4 elements.
Let us now illustrate some more subtle errors detected by e-acsl. Replace the
line 15 of Fig. 3 by a local array int c[4]; and complete the resulting program
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

int trace = c[0] + c[2};

4

free(c);

5

return 0;

6

7 }