/*@
…
loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m2)[i] == \at(((char*)m1)[i], Pre);
loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m1)[i] == \at(((char*)m2)[i], Pre);
loop assigns n, tmp, ((char*)m1)[0..\at(n,Pre)-1], ((char*)um2)[0..\at(n, Pre)-1], p, q;
…
@*/
You have the wrong loop assigns
. The loop assigns
annotations tells what memory locations have been modified at each iteration. The number of locations should typically increase as the loop progresses (in your case, as n
decreases). It is something like:
loop assigns n, tmp, ((char*)m1)[0..(\at(n, Pre) - n - 1)], ((char*)um2)[0..(\at(n, Pre) - n - 1)], p, q;
But my own proposal above may be off by one in one direction or another. I find it difficult to remember exactly how these “moving” loop assigns clauses work exactly.
Alternately, you may write a simpler, “static” loop assigns
annotation (like yours), and add the information about what hasn't changed yet in the loop invariant. This is what I usually do to circumvent my inability to remember how complex loop assigns
clauses work. That would be something like (untested):
/*@
…
loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m2)[i] == \at(((char*)m1)[i], Pre);
loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m1)[i] == \at(((char*)m2)[i], Pre);
loop invariant \forall integer i; (\at(n, Pre) - n) <= i < \at(n, Pre) ==> ((char*)m1)[i] == \at(((char*)m1)[i], Pre);
loop invariant \forall integer i; (\at(n, Pre) - n) <= i < \at(n, Pre) ==> ((char*)m2)[i] == \at(((char*)m2)[i], Pre);
loop assigns n, tmp, ((char*)m1)[0..\at(n,Pre)-1], ((char*)um2)[0..\at(n, Pre)-1], p, q;
…
@*/