loop assigns, part 2

This post shows various ways to specify the loop assigns which modifies at each step a pointer and its content. This is the answers to the exercise of the preceding post on this subject.

Context

Last week's post asked how to express a loop assigns for the following code:

void fill(char* a, char x) {
  for(;*a;a++)
    *a = x;

   return;
}

The difficulty here is that the pointer a is modified at each step of the loop, and that we must take this fact into account when writing the loop assigns

Very broad (but correct) annotations

Remember that (loop) assigns clauses are an overapproximation of the locations that are actually written. Thus, a first possibility is to say that each step can potentially modify any byte from the block pointed to by a (and a itself of course).

loop assigns a, a[..];

Since we do not specify any of the bounds in the range, we really mean that each step is allowed to modify any location reachable from (the current value of) a, in any direction. In fact, it is not too difficult to be slightly more precise: a is the upper bound of the locations that have been written to so far, so that the following clause is also correct:

loop assigns a, a[..(-1)];

However, this assignment is too broad: if we call fill with a parameter that points to the middle of a block, the loop assigns tells that the beginning of the block can be modified too. Let's see if we can do better.

Precise annotations

In fact, we want to say that before entering the current loop step, we have modified the set of locations that are between the initial (which is denoted as \at(a,Pre) in ACSL's terms) and the current value of a, the latter exlcuded. This can be done in ACSL by defining the set in comprehension: the ACSL expression below is literally the translation of the previous sentence.

loop assigns a, *{ p | char* p; \at(a,Pre) <= p < a };

Unfortunately, such definition is not handled by the Jessie plugin yet, and we can not use Frama-C to verify that it is indeed correct (at least, it is accepted by the parser, but that only means that this is a well-typed expression). In fact, Jessie is more comfortable with ranges of location, and we can try to use that, starting either from a and going backward, or from \at(a,Pre) and going forward:

loop assigns a, a[(\at(a,Pre)-a)..(-1)];

Alternative annotation, starting from the initial value of a:

loop assigns a, \at(a,Pre)[0..(a-\at(a,Pre)-1)];

This time, Jessie accepts to generate the proof obligation[1], but the automated theorem provers seem unable to handle it. In fact, This annotation alone is not provable, even if we assume that all pointer accesses are valid and no arithmetic overflow occurs. Why is that? Well I guess this will be the subject of the quizz for next post.

Notes

[1] The analyses have been made with Frama-C Boron and Why 2.27