--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on October 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP plugin report incorrect



> On 05 Oct 2015, at 17:32, Loïc Correnson <loic.correnson at cea.fr> wrote:
> 
> Your function *is* doing something, and the post-condition is exactly your loop invariant with (i == end), hence it finally holds.
> 	L.

But shouldn’t WP be unable to prove the loop invariant if the loop body is empty? The `swap(a+i, a+i)’ effectively does nothing, you can just comment it out. You can go even further and remove everything inside the loop, leaving us with:

/*@
 @ requires end >= start >= 0;
 @ requires \valid(a+(start..end-1));
 @ assigns a[start..end-1];
 @ ensures \forall integer m; (start <= m < end) ==> a[m] <= a[end-1];
 @ ensures Permut{Old,Here}(a, start, end-1);
 @*/
void bub_max(int* a, int start, int end) {
 /*@
   @ loop assigns i, a[start..end-1];
   @ loop invariant \forall integer m; (start <= m <= i) ==> a[m] <= a[i];
   @*/
 for (int i = start; i < end-1; i++) {
    // do nothing
 }

which still verifies. If I completely remove the loop and thus the invariant, it doesn’t verify. How can it possibly prove the loop invariant? As far as I understand the semantics of the loop invariant, this should not hold.

--
Christoph