--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on October 2008 ---
Thank you for the advice, it worked under the Helium release. After searching the ACSL_1.3 PDF i found the \separated(...) function. My question is if its posible to use it in a following manner : /*@ requires \separated(a, b); */ void array_cpy(int* a, int n, int* b); or do i have to be more specific, say like this: /*@ requires \forall int i,j; \separated(a[i] b[j]); */ void array_cpy(int* a, int n, int* b); Christoph ----- Original Message ----- From: Yannick Moy To: Claude March? Cc: frama-c-discuss@lists.gforge.inria.fr Sent: Thursday, October 09, 2008 4:25 PM Subject: Re: [Frama-c-discuss] Specification Examples Just a precision: With the next version of Frama-C, the separation of pointers into different regions is automatic (unless you prevent it with an option), so that your pointer parameters [a] and [b] belong indeed to different heap regions. Then, your code is proved right away. You may try option [-jc-opt -separation] to try it on the current version. Then, you will get PO at function call to prove these regions are indeed separated if the tool cannot figure it alone. -- Yannick On Thu, Oct 9, 2008 at 4:18 PM, Claude March? <Claude.Marche@inria.fr> wrote: Christoph Weber wrote: #2: in the second example the preservation of the loop invariant wont work /*@ requires 0 < n; requires \valid_range(a, 0, n-1) && \valid_range(b, 0, n-1); ensures \forall int k; 0 <= k < n ==> a[k] == b[k]; */ void array_cpy(int* a, int n, int* b){ /*@ loop invariant 0 <= i <= n && \forall int m; 0 <= m < i ==> a[m] == b[m]; */ for(int i = 0;i< n;i++){ a[i]=b[i]; } } What am I missing, to get the examples running? You must take into account the fact that arrays a and b might overlap, such as if you call array_cpy as array_cpy(t,10,t+1); in such a case your spec does not hold I think. - Claude -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex | _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss@lists.gforge.inria.fr http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -- 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/20081010/9de27eb9/attachment.htm