--- layout: fc_discuss_archives title: Message 69 from Frama-C-discuss on October 2008 ---
Hello again, I'm trying to explore a new example combining array_cpy(int* a, int n, int* b); and fill_int_array(int* first, int* last, int value). This one is called copy_int_array (int* first, int* last, int* result). DESCRIPTION: Copies the elements in the range [first,last) into a range beginning at result. Returns an iterator to the last element in the destination range. Parameters: first, last: Pointers to the initial and final positions of the searched sequence. The range used is [first,last), which contains all the elements between first and last, including the element pointed by first but not the element pointed by last. result Pointer to the initial position in the destination sequence. This shall not point to any element in the range [first,last). Return value: A pointer to the last element of the destination sequence where elements have been copied. CODE: /*@ predicate disjoint_arrays(int* a, int* b, integer i) = \forall integer k1, k2; 0 <= k1 < i && 0 <= k2 < i ==> a + k1 != b + k2; */ /*@ requires last > first; requires disjoint_arrays(first, result, last-first); requires \valid_range (first, 0, last-first-1); requires \valid_range (result, 0, last-first-1); ensures \forall integer i; 0 <= i < last-first ==> result[i] == first[i]; */ int* copy_int_array (int* first, int* last, int* result) { //@ ghost int* a = first; //@ ghost int* b = result; //@ ghost int length = last-first; /*@ loop invariant a <= first <= last; loop invariant b <= result <= b+length; loop invariant \forall integer k; 0 <= k < first-a ==> result[k] == first[k]; */ while (first!=last) *result++ = *first++; return result; } Up to this moment Jessie is unable to solve it entirely. Am I missing something or is it due to my Hydrogen version. Greets Christoph -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081017/10c0cc6c/attachment.html