--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on October 2008 ---
Hi, There is indeed a solution if you only intend to work with the Jessie plugin. Since this plugin works with a typed memory model by default (when there are no pointer casts and unions), you may express separation with the following predicate: /*@ predicate disjoint_arrays(char *a, char *b, integer i) = @ \forall integer k1, k2; @ 0 <= k1 < i && 0 <= k2 < i ==> a + k1 != b + k2; @*/ HTH, Yannick On Fri, Oct 10, 2008 at 1:41 PM, Christoph Weber < Christoph.Weber@first.fraunhofer.de> wrote: > Thats a pitty, > > but is there any posibility to ask explicitly something about pointer > related stuff in the Jessie plugin besides \valid... to circumvent the > existing problems? > > I'd like to verify it within a requires clause and not by using an option, > perhaps by defining my own function. > > Christoph > > ----- Original Message ----- > *From:* Yannick Moy <yannick.moy@gmail.com> > *To:* Christoph Weber <Christoph.Weber@first.fraunhofer.de> > *Cc:* frama-c-discuss@lists.gforge.inria.fr > *Sent:* Friday, October 10, 2008 1:13 PM > *Subject:* Re: [Frama-c-discuss] Specification Examples > > 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 > > ------------------------------ > > _______________________________________________ > 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/c832ac4f/attachment.htm