--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on October 2015 ---
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