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] Pass by reference

  • Subject: [Frama-c-discuss] Pass by reference
  • From: michaelschausten at googlemail.com (Michael Schausten)
  • Date: Thu, 07 Oct 2010 10:48:11 +0200
  • In-reply-to: <AANLkTinK+zk+8JDG3LrKSWPd=5U_szjQwhogRPuXBHt=@mail.gmail.com>
  • References: <AANLkTinK+zk+8JDG3LrKSWPd=5U_szjQwhogRPuXBHt=@mail.gmail.com>
  Hello ?o?n Th?nh Nam

I think the main problem is that Frama-C uses C and not C++, a C 
compiler already won't understand your code, therefore you can't parse 
it with frama-c.

Sincerely,



Am 07.10.2010 10:37, schrieb nam nam:
> Dear all,
>
> I wonder whether Frama-C can help me to prove functions that contain 
> passing by reference or not.
> I have found in ACSL  manual and also your mailing list but I did not 
> find anything like this.
>
> For example,
> /*@ensures \result == 1;
> */
> int temp(int& n) // Frama-C announces parsing error here.
> {
>     n = 1;
>     return n;
> }
>
> Thank you.
> -- 
> ?o?n Th?nh Nam
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20101007/96394fdc/attachment.htm>