--- layout: fc_discuss_archives title: Message 54 from Frama-C-discuss on October 2008 ---
Hi, Sorry, I did only check on the current unreleased version. I'll check on a released version next time. This will be available in the next release so. Yannick On Tue, Oct 14, 2008 at 12:16 PM, Jens Gerlach < jens.gerlach@first.fraunhofer.de> wrote: > Dear Yannik, > > >> But if I am using the Pre Label I don't meet the ensures requirements, or >> at least I don't get a green bullet. >> > > 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). > > 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]; > } > > > I just run this example under Helium (Mac OS X) (adding the disjoint_arrays > predicate) and received the following error message > > running gcc -C -E -I. array.c > File array.c, line 7, characters 50-63: > Error during analysis of annotation: logic label `Pre' not found > array.c:7: Warning: ignoring logic specification of function array_cpy > Parsing > > Best regards > > Jens Gerlach > > 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/155292f7/attachment.html