2021-03-05 02:53 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001853Frama-CKernelpublic2015-03-17 22:18
Assigned Toyakobowski 
PlatformlinuxOS ubuntu 12.04 LTSOS Version12.04 LTS
Product VersionFrama-C Neon-20140301 
Target VersionFixed in VersionFrama-C Sodium 
Summary0001853: bogus syntax error with doxygen
DescriptionI 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.
Steps To Reproducecreate 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.
TagsNo tags attached.
Attached Files




virgile (developer)

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.


signoles (manager)

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: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-June/001275.html. 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.


yakobowski (manager)

Fix committed to master branch.

-Issue History
Date Modified Username Field Change
2014-07-23 22:21 billyPilgrim New Issue
2014-07-28 16:47 virgile Note Added: 0005315
2014-07-28 16:48 virgile Severity major => feature
2014-07-28 16:48 virgile Status new => confirmed
2014-08-04 15:51 signoles Note Added: 0005357
2014-10-27 00:53 yakobowski Assigned To => yakobowski
2014-10-27 00:53 yakobowski Status confirmed => assigned
2014-11-28 18:37 yakobowski Source_changeset_attached => framac master 4d1335e8
2014-11-28 18:37 yakobowski Note Added: 0005579
2014-11-28 18:37 yakobowski Status assigned => resolved
2014-11-28 18:37 yakobowski Resolution open => fixed
2015-03-17 22:17 signoles Fixed in Version => Frama-C Sodium
2015-03-17 22:18 signoles Status resolved => closed
+Issue History