--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on October 2008 ---
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/<http://www.lri.fr/%7Emarche/> > 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 -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081009/bfceea37/attachment.html