--- layout: fc_discuss_archives title: Message 53 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,

We found that automatic separation is usually what you need, although there
will be an option -jessie-no-regions to avoid such splitting of memory.

Given a function signature:

void array_cpy(int* a, int n, int* b)

the regions inferred for [a] and [b] depend on the code of function
[array_cpy] and the functions it calls (possibly recursively). These regions
are assumed different, unless the code explicitly aliases them, say by
assigning [a] to [b]. Then, the code of function [array_cpy] can be easily
verified in this separated context, while it can still be called in a
context where [a] and [b] may alias if:

1) [a] and [b] are only read through in a call to [array_cpy]
2) [a] and [b] are accessed at separated locations

There will be an extensive section of the Jessie manual dedicated to this
matter.
Best regards,

Yannick


On Tue, Oct 14, 2008 at 11:27 AM, Jens Gerlach <
jens.gerlach@first.fraunhofer.de> wrote:

>  Hello Yannik,
>
> I do not quite understand your remarks automatic division of the heap.
>
>
> as I told you, the normal way of treating separation in Jessie is to divide
> heap into regions automatically, which will become the default in the next
> release. With only one region for memory, your example is proved with any of
> Z3, Alt-Ergo and Simplify (not Yices though).
>
>
> Does this mean that in a future release of Frama-C it is assumed that the
> two pointers a and b
> in a declaration like
>
> void array_cpy(int* a, int n, int* b)
>
> point to disjoint memory regions?
> I'd rather prefer the explicit declaration with the disjoint_arrays
> predicate provided by you.
>
> Best regards
>
> Jens Gerlach
> Fraunhofer FIRST
>
>
>
> To prove instead that the value of [a] after copying is the same as the
> value of [b] before, you need to strengthen the loop invariant like follows,
> to assess that all of [b] does not change during the loop.
>
> /*@ requires 0 < n;
>   @ requires \valid_range(a, 0, n-1) && \valid_range(b, 0, n-1);
>   @ requires disjoint_arrays(a, b, n);
>   @ ensures  \forall int k; 0 <= k < n ==> a[k] == \at(b[k],Pre);
>   @*/
> void array_cpy(int* a, int n, int* b)
> {
>    /*@ loop invariant 0 <= i <= n;
>      @ loop invariant \forall int m; 0 <= m < n  ==> b[m] == \at(b[m],Pre);
>      @ loop invariant \forall int m; 0 <= m < i  ==> a[m] == b[m];
>      @*/
>    for (int i = 0; i < n; i++)
>      a[i] = b[i];
> }
>
> With these annotations, Z3, ALt-Ergo and Simplify still prove your function
> (not Yices).
>
>
>>
>> Currently I'm stuck with an other Problem. Within some annotated string.h
>> examples I found a dereferenced \result.
>>
>> Attempts to apply it to my example will result in the following error.
>>
>> Fatal error: exception Assert_failure("src/jessie/interp.ml", 336, 14)
>>
>> do I get it due to my Hydrogen version ?
>>
>
> Most probably, yes. There was such a problem with derefencing \result and
> it was solved. The best way to track this kind of problem is to fill in a
> bug report on the Frama-C public BTS, so that you get a precise answer when
> the bug gets fixed.
>
> HTH.
>
> --
> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081014/6e2660fd/attachment.html