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
LoopCurrent
andLoopEntry
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 therequires
andassumes
clauses are evaluated). It is thus equivalent toPre
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 inensures
,assigns
,allocates
orfrees
clauses, and refer to the state at the end of the contract.