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

[Frama-c-discuss] Specification Examples



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 
  To: Christoph Weber 
  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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081010/ac4caf8c/attachment.htm