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

[Frama-c-discuss] Specification Examples



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);


Christoph

  ----- Original Message ----- 
  From: Yannick Moy 
  To: Claude March? 
  Cc: frama-c-discuss@lists.gforge.inria.fr 
  Sent: Thursday, October 09, 2008 4:25 PM
  Subject: Re: [Frama-c-discuss] Specification Examples


  Just a precision:

  With the next version of Frama-C, the separation of pointers into different regions is automatic (unless you prevent it with an option), so that your pointer parameters [a] and [b] belong indeed to different heap regions. Then, your code is proved right away. You may try option [-jc-opt -separation] to try it on the current version. Then, you will get PO at function call to prove these regions are indeed separated if the tool cannot figure it alone.

  --
  Yannick



  On Thu, Oct 9, 2008 at 4:18 PM, Claude March? <Claude.Marche@inria.fr> wrote:



    Christoph Weber wrote:

      #2: in the second example the preservation of the loop invariant wont work



      /*@  requires 0 < n;   requires \valid_range(a, 0, n-1) && \valid_range(b, 0, n-1);
       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];     } }


      What am I missing, to get the examples running?



    You must take into account the fact that arrays a and b might overlap, such as if you call array_cpy as

     array_cpy(t,10,t+1);

    in such a case your spec does not hold I think.

    - Claude

    -- 
    Claude March?                          | tel: +33 1 72 92 59 69
    INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
    Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
    4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
    F-91893 ORSAY Cedex                    |







    _______________________________________________
    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/9de27eb9/attachment.htm