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