Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Specification Examples

  • Subject: [Frama-c-discuss] Specification Examples
  • From: yannick.moy at gmail.com (Yannick Moy)
  • Date: Fri Oct 10 13:13:54 2008
  • In-reply-to: <1B3FA18004D74D5787DB01AD1EB95900@AHARDPLACE>
  • References: <4FA912B7D4D8468FBACF5B5DDE198385@AHARDPLACE> <48EE12A8.8020908@inria.fr> <14791e30810090725i702ded18gf548d53abb9beeee@mail.gmail.com> <C88F4E451E884829944B1A79F874868C@AHARDPLACE> <20081010124942.4f8a52db@is005115> <1B3FA18004D74D5787DB01AD1EB95900@AHARDPLACE>
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