--- layout: fc_discuss_archives title: Message 43 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 and a thank you for the help,

but I like to continue questioning where I stopped.

You remember the array_cpy:
/*@
 requires 0 < n;
 requires \valid_range(a, 0, n-1) && \valid_range(b, 0, n-1)&& disjoint_arrays(a, b, n);
 ensures  \forall int k; 0 <= k < n ==> a[k] == b[k];
*/
void array_cpy(int* a, int n, int* b)
{
    /*@
     loop invariant 0 <= i <= n && \forall int m; 0 <= m < i  ==> a[m] == b[m];
    */
    for (int i = 0;i < n;i++)
    {
        a[i] = b[i];
    }
}

This works fine with the Hydrogen-version on Win 32 and the Z3 prover. On the Helium edition on OSX it terminates successfully with CVC3 (Z3 not aviable). Now I'd like to know:
- what has to be done or added to let ergo v0.8 or simplify verify it as well.
- array_cpy is only partial specified on my opinion the ensures clause has to be altered to
    ensures  \forall int k; 0 <= k < n ==> a[k] == \old(b[k]);
using this I receive an error due to preservation of loop invariant. I think  the comparison in the loop invariant has to be altered to 
     a[m] == \at(b[m],Old);
but FramaC will return
    File array_test.c, line 28, characters 80-93:
    Error during analysis of annotation: logic label `Old' not found
    array_test.c:29: Warning: ignoring logic loop annotation
I tried a bit but I where unable to cheat my way around.

Thanks in advance

Christoph
  ----- Original Message ----- 
  From: Yannick Moy 
  To: Christoph Weber 
  Cc: frama-c-discuss@lists.gforge.inria.fr ; Juan Soto 
  Sent: Friday, October 10, 2008 2:05 PM
  Subject: Re: [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 
      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


    _______________________________________________
    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/20081013/128b03f3/attachment.htm