--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on November 2008 ---
Hi, You need to express that [copy] may modify the content of the array pointed-to by dest, which can be as simple as //@ assigns dest[..]; or with more precision //@ assigns dest[0..last-first]; HTH, Yannick On Mon, Nov 10, 2008 at 1:58 PM, Christoph Weber < Christoph.Weber@first.fraunhofer.de> wrote: > Hello again, > > this time I am doing some exercises with Hydrogen. > > I am using the copy algorithm to implement a rotate function: > It copies the values of the elements in the range [first,last) to the range > positions > beginning at result, but rotating the order of the elements in such a way > that the > element pointed by middle becomes the first element in the resulting range. > > rotate_copy=========================== > > #include "copy.h" > #include "predicates.h" /*@ > requires last > middle >= first; > requires \valid_range (first, 0, last-first-1); > requires \valid_range (dest, 0, last-first-1); > requires disjoint_arrays(first, dest, last-first); > > > ensures \forall integer i; 0 <= i < middle-first ==> dest[i] == middle[i]; > ensures \forall integer i; middle-first <= i < last-middle ==> dest[i] == > first[i]; > */ > int* rotate_copy (int* first, int* middle, int* last, int* dest ) { > dest = copy (middle, last, dest); > return copy (first, middle, dest); > } > ========================================= > copy.h==================================== > /*@ > requires last > first; > requires disjoint_arrays(first, dest, last-first); > requires \valid_range (first, 0, last-first-1); > requires \valid_range (dest, 0, last-first-1); > assigns \nothing; > ensures \forall integer i; 0 <= i < last-first ==> dest[i] == first[i]; > */ > int* copy (int* first, int* last, int* dest); > ========================================= > copy.c==================================== > #include "copy.h" > int* copy (int* first, int* last, int* dest) { > int* it1 = first; > int* it2 = dest; > /*@ > loop invariant first <= it1 <= last; > loop invariant it2 - dest == it1 - first; > loop invariant dest <= it2 <= dest + (last-first); > loop invariant \forall integer k; 0 <= k < it1-first ==> first[k] == > dest[k]; > */ > while (it1 != last) > { > *it2++ = *it1++; > } > return it2; > } > > The Problems are as followed: > > The assigns clause in copy.h is nonesense but "assigns dest " will work > even less. () > > with assigns \nothing i get copy.c proven but rotate_copy fails with > preconditions. > > My qeuestion is: What has to be added to get it through. > > > > Cheers Christoph > > _______________________________________________ > 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/20081110/555f8a2f/attachment.html