--- layout: fc_discuss_archives title: Message 111 from Frama-C-discuss on October 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] unbound identifier \result



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