--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on October 2008 ---
Hi, Indeed, \separated is not implemented in the version of Frama-C released, and \base_addr is not yet implemented in the Jessie plugin (although it is implemented in Frama-C). Hopefully the next release will solve these problems :0) Yannick On Fri, Oct 10, 2008 at 1:07 PM, Christoph Weber < Christoph.Weber@first.fraunhofer.de> wrote: > Hello, > > i thought so and i tried as well but it seams as if the memory related > functions wont work properly or are not implemented. > > the usage of requires > //@ \separated(a+(..),b+(..)); > will result in > File "array_test.c", line 18, characters 89-99: lexical error, illegal > escape sequence \separated > > the line > //@ requires \base_addr(a) != \base_addr(b); > will cause > Fatal error: exception Assert_failure("src/jessie/interp.ml", 455, 23) > > am I missing something? > > Christoph > > ----- Original Message ----- From: "Virgile Prevosto" < > virgile.prevosto@cea.fr> > To: <frama-c-discuss@lists.gforge.inria.fr> > Sent: Friday, October 10, 2008 12:49 PM > Subject: Re: [Frama-c-discuss] Specification Examples > > > Hello, > > Le ven 10 oct 2008 11:39:59 CEST, > "Christoph Weber" <Christoph.Weber@first.fraunhofer.de> a ?crit : > > 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); >> >> >> > Neither ;-) > > - \separated(a,b) indicates that the locations pointed to by a and b > (both seen as pointer to int) do not overlap. > > - \separated(a[i],b[j]) is ill-formed: \separated takes addresses as > arguments not the values themselves. You should use > \separated(a+i,b+j). > > Note that the latter is equivalent to the following precondition which > uses (indefinite) ranges of addresses: > //@ requires \separated(a+(..),b+(..)); > > > -- > E tutto per oggi, a la prossima volta. > Virgile > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss@lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > > > _______________________________________________ > 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/20081010/40d11935/attachment.html