Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001853Frama-CKernelpublic2014-07-23 22:212015-03-17 22:18
ReporterbillyPilgrim 
Assigned Toyakobowski 
PrioritynormalSeverityfeatureReproducibilityalways
StatusclosedResolutionfixed 
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

- Relationships

-  Notes
(0005315)
virgile (developer)
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.
(0005357)
signoles (manager)
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: 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.
(0005579)
yakobowski (manager)
2014-11-28 18:37

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 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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker