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

[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/<http://www.lri.fr/%7Emarche/>
> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081009/bfceea37/attachment.html