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

[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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081010/40d11935/attachment.html