--- layout: fc_discuss_archives title: Message 53 from Frama-C-discuss on October 2008 ---
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