Understanding Frama-C logic labels

Question

I have some troubles when I try to use the default logic labels LoopEntry and LoopCurrent. Here is a simple example the different provers (alt-ergo, coq, cvc3, z3) I use are not able to prove :

/*@ requires n > 0;*/
void f(int n){
    int i = 0;
    /*@ loop invariant \at(i,LoopEntry) == 0;
      @ loop invariant \at(i,LoopCurrent) >= \at(i,LoopEntry);
      @ loop invariant 0 <= i <= n;
      @ loop assigns i;
      @ loop variant n-i;
    */
    while(i < n){
        i++;
    }
}

In particular, the first and second invariants are not proved (no problem with the others). Now if I modify this simple example by adding a label "label" after the declaration/definition of i and if I refer to that label, and change LoopCurrent by Here (which gives this snippet :

/*@ requires n > 0;*/
void f(int n){
    int i = 0;
    label : ;
    /*@ loop assigns i;
      @ loop invariant \at(i,label) == 0;
      @ loop invariant \at(i,Here) >= \at(i,label);
      @ loop invariant 0 <= i <= n;
      @ loop variant n-i;
    */
    while(i < n){
        i++;
    }
}

)

now everything is proved.

I found the documentation about Acsl default logic labels quite easy to understand and I expected the first example to be proved as the second. Could you explain where does the problem come from?

Roo

PS1 : what does Pre refer to when used in a loop clause? The state before first loop iteration or the previous iteration??

PS2 : I'm using Frama-C Fluorine, but maybe I didn't upgrade for every minor updates

Answer 1

LoopCurrent and LoopEntry are indeed not supported by WP in Fluorine. This is fixed in the development version (see http://bts.frama-c.com/view.php?id=1353), and should appear in the next release.

Regarding the other pre-defined labels,

• Pre always refers to the state at the beginning of the function.
• Old can only be used in a contract, and refers to the pre-state of this contract (i.e. the state in which the requires and assumes clauses are evaluated). It is thus equivalent to Pre for a function contract, but not for a statement contract (unless you make a contract enclosing the main block of your function).
• Here means the program point where the corresponding annotation is evaluated. In a contract, its meaning depends on the clause in which it appears.
• Post can only be used in ensures, assigns, allocates or frees clauses, and refer to the state at the end of the contract.