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: yannick.moy at gmail.com (Yannick Moy)
  • Date: Fri Oct 31 16:29:57 2008
  • In-reply-to: <2C4881A52B5440438647B735A70019B2@AHARDPLACE>
  • References: <2C4881A52B5440438647B735A70019B2@AHARDPLACE>
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