--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on October 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Pass by reference



  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>