--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on October 2008 ---
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