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: doan.thanh.nam.1988 at gmail.com (nam nam)
  • Date: Thu, 7 Oct 2010 16:37:06 +0800
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20101007/f8df21a9/attachment.htm>