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