Frama-C Bug Tracking System - Frama-C
View Issue Details
0001853Frama-CKernelpublic2014-07-23 22:212015-03-17 22:18
linux ubuntu 12.04 LTS12.04 LTS
Frama-C Neon-20140301 
Frama-C Sodium 
0001853: bogus syntax error with doxygen
I have several header files that contain: /*@} strings beginning comments. This will cause frama-c to stop due to a syntax error. It can be fixed by inserting a space between the '*' and the '@'. I don't know if that will result in ill-formed doxygen (I didn't create the file and am not a doxygen user), but the parser does choke on it.
create a header file and put in a comment, starting in column 1 /*@} End of pub_func */ and it will fail. replace with: /* @} End of pub_func */ and all is well.
No tags attached.
Issue History
2014-07-23 22:21billyPilgrimNew Issue
2014-07-28 16:47virgileNote Added: 0005315
2014-07-28 16:48virgileSeveritymajor => feature
2014-07-28 16:48virgileStatusnew => confirmed
2014-08-04 15:51signolesNote Added: 0005357
2014-10-27 00:53yakobowskiAssigned To => yakobowski
2014-10-27 00:53yakobowskiStatusconfirmed => assigned
2014-11-28 18:37yakobowskiNote Added: 0005579
2014-11-28 18:37yakobowskiStatusassigned => resolved
2014-11-28 18:37yakobowskiResolutionopen => fixed
2015-03-17 22:17signolesFixed in Version => Frama-C Sodium
2015-03-17 22:18signolesStatusresolved => closed

2014-07-28 16:47   
Actually, you can deactivate parsing of annotations with -no-annot. With that option, /*@ will not be interpreted by Frama-C as an ACSL annotation, hence '/*@ }' will not create a syntax error. If you want to have both Doxygen comments and ACSL annotations, it is possible to change the character that introduces ACSL annots from '@' to e.g. '^', but only programmatically in a script/plugin. There is no command-line option for that.
2014-08-04 15:51   
This was discussed on the frama-c-discuss mailing list in 2009. At this time, Benjamin Monate wrote a script to replace '@' by another character. The script is here: It is compatible with Frama-C Beryllium beta-1, a very old version of Frama-C, but I guess it could be modified easily to be compatible with more recent versions of Frama-C.
2014-11-28 18:37   
Fix committed to master branch.