Frama-C/WP not able to prove loop invariant with \at

Question

I'm having trouble proving 2 loop invariants:

    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);

I'm guessing \at isn't working for arrays as i expect.

There is a similar function in ACSL by Example (page 68, swap_ranges), that uses this, but, as stated, they were not able to prove this particular function with the WP plugin. I tried it on my machine and indeed it is not able to prove the same invariant.

Full code

/*
 * memswap()
 *
 * Swaps the contents of two nonoverlapping memory areas.
 * This really could be done faster...
 */

#include "string.h"

/*@
    requires n >= 1;
    requires \valid(((char*)m1)+(0..n-1));
    requires \valid(((char*)m2)+(0..n-1));
    requires \separated(((char*)m1)+(0..n-1), ((char*)m2)+(0..n-1));
    assigns ((char*)m1)[0..n-1];
    assigns ((char*)m2)[0..n-1];
    ensures \forall integer i; 0 <= i < n ==> ((char*)m1)[i] == \old(((char*)m2)[i]);
    ensures \forall integer i; 0 <= i < n ==> ((char*)m2)[i] == \old(((char*)m1)[i]);
@*/
void memswap(void *m1, void *m2, size_t n)
{
    char *p = m1;
    char *q = m2;
    char tmp;

    /*@
        loop invariant 0 <= n <= \at(n, Pre);
        loop invariant p == m1+(\at(n, Pre) - n);
        loop invariant q == m2+(\at(n, Pre) - n);
        loop invariant (char*)m1 <= p <= (char*)m1+\at(n, Pre);
        loop invariant (char*)m2 <= q <= (char*)m2+\at(n, Pre);
        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;
        loop variant n;
    @*/
    while (/*n--*/ n) {
        tmp = *p;
        *p = *q;
        *q = tmp;

        p++;
        q++;

        n--; // inserted code
    }
}

EDIT

Im using Frama-C Oxygen release and tried automatic proving with alt-ergo(0.94) and cvc3(2.4.1)

output from frama-c:

cvc3:

[wp] [Cvc3] Goal store_memswap_loop_inv_7_established : Valid
[wp] [Cvc3] Goal store_memswap_loop_inv_6_established : Valid
[wp] [Cvc3] Goal store_memswap_loop_inv_7_preserved : Unknown
[wp] [Cvc3] Goal store_memswap_loop_inv_6_preserved : Unknown

alt-ergo:

[wp] [Alt-Ergo] Goal store_memswap_loop_inv_7_established : Valid
[wp] [Alt-Ergo] Goal store_memswap_loop_inv_6_established : Valid
[wp] [Alt-Ergo] Goal store_memswap_loop_inv_7_preserved : Timeout
[wp] [Alt-Ergo] Goal store_memswap_loop_inv_6_preserved : Timeout

Answer 1

/*@
…
    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;
…
@*/