--- layout: fc_discuss_archives title: Message 40 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,

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