--- layout: fc_discuss_archives title: Message 50 from Frama-C-discuss on October 2008 ---
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 -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081014/21f1d34a/attachment.html