--- layout: fc_discuss_archives title: Message 122 from Frama-C-discuss on October 2008 ---
Hi, There is indeed a problem with the changes we made in the memory model of the Jessie plugin. I think we'll have to patch the current release to overcome this problem. If so, we will announce it on this list soon. Yannick On Thu, Oct 30, 2008 at 9:01 AM, Christoph Weber < Christoph.Weber@first.fraunhofer.de> wrote: > Hello again, > > Thank You and granulations for the latest release. > > But I have some problems to get started. Lets start with an example. > Following Function in separate files: > > > fill.h: > > /*@ > requires valid_range(first, last); > requires \valid_range(first, 0, last-first -1); > behavior is_not_empty: > assumes not_empty_range(first, last); > ensures \forall integer i; > 0 <= i < last-first ==> first[i] == value; > */ > void fill (int* first, int* last, int value ); > > fill.c: > > #include > "fill.h" > void fill (int* first, int* last, int value ) { > int* it = first; > /*@ > loop invariant first <= it <= last; > loop invariant \forall integer k; 0 <= k < it - first ==> first[k] == > value; > */ > while (it != last) > *it++ = value; > } > > I call Jessie: > frama-c -jessie-analysis -jessie-int-model exact -jessie-no-regions > -jessie-gui fill.c > > Now the problems: > -the loop invariant cannot be preserved, => am I missing an option or an > annotation (it went fine on H and He) > -the declared int* it causes problems in pointer dereferencing > -Z3, CVC3, and Yices get stuck and wont abort, the timeout never worked on > any release yet (on my pc) > > > I hope for help > > Cheers > > > _______________________________________________ > 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/20081030/973263ec/attachment.html