--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on December 2015 ---
Hi, My only possible answer is that everything is proved with (on-going, not yet released) Magnesium version and alt-ergo 0.99.1 May I suggest you to upgrade to, let say, opam versions ? Sorry, I donât have time right now to investigate on older versions. L. > Le 9 déc. 2015 à 17:00, Timo Kamph <timo.kamph at tuhh.de> a écrit : > > /*@ 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); > } > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20151209/c54be375/attachment-0001.html>