--- layout: fc_discuss_archives title: Message 50 from Frama-C-discuss on October 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Specification Examples



Hello Yannik,

I do not quite understand your remarks automatic division of the heap.

>
> as I told you, the normal way of treating separation in Jessie is to  
> divide heap into regions automatically, which will become the  
> default in the next release. With only one region for memory, your  
> example is proved with any of Z3, Alt-Ergo and Simplify (not Yices  
> though).

Does this mean that in a future release of Frama-C it is assumed that  
the two pointers a and b
in a declaration like

	void array_cpy(int* a, int n, int* b)

point to disjoint memory regions?
I'd rather prefer the explicit declaration with the disjoint_arrays  
predicate provided by you.

Best regards

Jens Gerlach
Fraunhofer FIRST

>
>
> To prove instead that the value of [a] after copying is the same as  
> the value of [b] before, you need to strengthen the loop invariant  
> like follows, to assess that all of [b] does not change during the  
> loop.
>
> /*@ requires 0 < n;
>   @ requires \valid_range(a, 0, n-1) && \valid_range(b, 0, n-1);
>   @ requires disjoint_arrays(a, b, n);
>   @ ensures  \forall int k; 0 <= k < n ==> a[k] == \at(b[k],Pre);
>   @*/
> void array_cpy(int* a, int n, int* b)
> {
>    /*@ loop invariant 0 <= i <= n;
>      @ loop invariant \forall int m; 0 <= m < n  ==> b[m] ==  
> \at(b[m],Pre);
>      @ loop invariant \forall int m; 0 <= m < i  ==> a[m] == b[m];
>      @*/
>    for (int i = 0; i < n; i++)
>      a[i] = b[i];
> }
>
> With these annotations, Z3, ALt-Ergo and Simplify still prove your  
> function (not Yices).
>
>
> Currently I'm stuck with an other Problem. Within some annotated  
> string.h examples I found a dereferenced \result.
>
> Attempts to apply it to my example will result in the following error.
>
> Fatal error: exception Assert_failure("src/jessie/interp.ml", 336, 14)
>
> do I get it due to my Hydrogen version ?
>
> Most probably, yes. There was such a problem with derefencing  
> \result and it was solved. The best way to track this kind of  
> problem is to fill in a bug report on the Frama-C public BTS, so  
> that you get a precise answer when the bug gets fixed.
>
> HTH.
>
> -- 
> Yannick
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss@lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081014/21f1d34a/attachment.html