--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on October 2008 ---
----- Original Message ----- From: Christoph Weber To: Christoph Weber Sent: Tuesday, October 14, 2008 10:07 AM Subject: Re: New Specification Examples Never mind, problem has been solved, thanks anyway ----- Original Message ----- From: Christoph Weber To: frama-c-discuss@lists.gforge.inria.fr Sent: Tuesday, October 14, 2008 9:38 AM Subject: New Specification Examples 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/dca6fe18/attachment.htm