--- layout: fc_discuss_archives title: Message 111 from Frama-C-discuss on October 2008 ---
Hello, I wonder if this is a known bug: I have a function: int* copy_int_array (int* first, int* last, int* dest) and I have an Annotation: /*@ 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); ensures \forall integer i; 0 <= i < last-first ==> dest[i] == first[i]; */ When I separate implementation and annotation in .c and .h files and I try to compile I get following message File "copy.jc", line 91, characters 10-17: typing error: unbound identifier \result Failed to run: jessie -why-opt -split-user-conj -locs copy.cloc copy.jc Error occurs in both Versions Greets Christoph -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081027/fa789c99/attachment.htm