Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] unbound identifier \result

  • Subject: [Frama-c-discuss] unbound identifier \result
  • From: Christoph.Weber at first.fraunhofer.de (Christoph Weber)
  • Date: Mon Oct 27 15:57:34 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