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,

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