Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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

  • Subject: [Frama-c-discuss] WP: Sodium version cannot prove a property that Neon version can prove
  • From: timo.kamph at tuhh.de (Timo Kamph)
  • Date: Wed, 9 Dec 2015 17:00:36 +0100
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