--- layout: fc_discuss_archives title: Message 129 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



Hi,

Yes, it is a known bug, due to an incorrect generation of default assigns
clause. To avoid it, just give an assigns clause to your function.

Thanks for reporting it!

Yannick

On Mon, Oct 27, 2008 at 3:57 PM, Christoph Weber <
Christoph.Weber@first.fraunhofer.de> wrote:

>  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
>
> _______________________________________________
> 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/20081031/47e5d55e/attachment-0001.html