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


Christoph Weber wrote:
> 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.

You have to improve ergo and simplify :-)

One advice is to use "integer" instead of ints in your annotations:

ensures  \forall integer k; 0 <= k < n ==> a[k] == b[k];

and so on.

> - 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.

Old does not mean anything in loop invariants. You have to use Pre:
a[m] == \at(b[m],Pre)