--- layout: fc_discuss_archives title: Message 6 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



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>