loop assigns, part 2

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.