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

[Frama-c-discuss] WP: Sodium version cannot prove a property that Neon version can prove



Hello,

I am following the Jessie tutorial by Nikolai Kosmatov et al., but I am
using WP instead of Jessie. All the given tasks work as expected except
for question 6. The code is given below. The WP version of Frama-C
Neon-20140301 can prove all VCs, but the version of Frama-C
Sodium-20150201 can not. It fails to prove that the array is sorted. The
external prover used in both cases is alt-ergo 0.95.2.

Is this a bug in WP or is there something wrong with the code that is
uncovered only in the latest version?


/*@ predicate sorted(int* arr, integer length) =
      \forall integer i, j; 0 <= i <= j < length ==> arr[i] <= arr[j];

    predicate mem(int elt, int* arr, integer length) =
      \exists integer i; 0 <= i < length && arr[i] == elt;
*/

/*@ requires sorted(arr, len);
    requires len >= 0;
    requires \valid(arr+(0..(len-1)));

    assigns \nothing;

    behavior exists:
      assumes mem(query, arr, len);
      ensures 0 <= \result < len;
      ensures arr[\result] == query;

    behavior not_exists:
      assumes ! mem(query, arr, len);
      ensures \result == -1;
*/
int find_array(int* arr, int len, int query);

void main() {
  int array[] = {0, 4, 5, 5, 7, 9};
  /*@ assert sorted((int*)array, 6); */
  int idx = find_array(array, 6, 7);
  /*@ assert idx == 4; */
  idx = find_array(array, 6, 5);
}



Another interesting fact is that the second call of find_array is
necessary for the prove to fail. If I comment it out, both versions can
prove that the array is sorted.

Regards,
Timo