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

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