--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on October 2010 ---
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>