--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on October 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Specification Examples



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