--- layout: fc_discuss_archives title: Message 14 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



Hello,

I’ve been trying to get a working bubble sort implementation to verify using the latest frama-c and WP plugin. After failing for a few days, I tried narrowing my problems down to simpler tasks. The following code is supposed to(!) bubble up the maximum value of the array to the position a[end-1] of the array, but notice that I intentionally modified the code so that it doesn’t change the array at all. Nevertheless, the WP plugin reports valid for all the proof goals, including the post-condition. Am I missing something obvious here?

/*@ requires \valid(i) && \valid(j);
  @ assigns *i, *j;
  @ ensures *i == \old(*j);
  @ ensures *j == \old(*i);
  @*/
void swap(int* i, int* j) {
  int tmp = *i;
  *i = *j;
  *j = tmp;
}

/*@
  @ 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];
  @*/
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++) {
    if (a[i] > a[i+1]) {
      swap(a+i, a+i);
    }
  }
}

--
Christoph