--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on November 2008 ---
Hi, and thank you for the help. I added an assigns clause and a loop assigns but the post-condition cannot be proven (Hydrogen). Is there something else missing or is it due to the Hydrogen. Christoph ----- Original Message ----- From: Yannick Moy To: Christoph Weber Cc: frama-c-discuss@lists.gforge.inria.fr Sent: Monday, November 10, 2008 11:49 PM Subject: Re: [Frama-c-discuss] Composition of COMPLEX Contracts 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/20081111/af6386c6/attachment.html