--- layout: fc_discuss_archives title: Message 47 from Frama-C-discuss on October 2008 ---
Hello, besides the problems I described in my last Mail (dereferencing of \result and Labeling inside loops), I'd like to alter the ranging of my array into a c++ stl Style, meaning (int* first, int* last, ...). So far ok, but: /*@ requires last >= first; requires \valid_range(first, 0, last-first-1); behavior is_not_empty: assumes last > first; ensures \forall integer i; 0 <= i < last-first ==> first [i] == value; behavior is_empty: assumes last == first; ensures last == first; */ void fill_int_array (int* first, int* last, int value ) { //@ ghost int* a = first; /*@ loop invariant a <= first <= last; loop invariant \forall integer k; 0 <= k < first-a ==> a[k] == value; */ while (first != last) *first++ = value; } In this example the ensurance of the postcondition does not work due to the changing value of first. Attempts to circumvent this with: ensures \forall integer i; 0 <= i < last-first ==> *(\old(first)+i) == value; have failed as well (to meet the postcondition in the Jessie-gui) Is there a possibility to allocate the old first or is this error due to the limitations of jessie and pals. Christoph -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081014/8dd46ab9/attachment.html