View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|
0001800 | Frama-C | Kernel | public | 2014-06-05 17:02 | 2014-06-06 00:15 | ||||||||
Reporter | Ian | ||||||||||||
Assigned To | virgile | ||||||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||||||
Status | assigned | Resolution | open | ||||||||||
Platform | OS | Ubuntu | OS Version | ||||||||||
Product Version | Frama-C Neon-20140301 | ||||||||||||
Target Version | Fixed in Version | ||||||||||||
Summary | 0001800: Cannot use quotes in comments in annotations | ||||||||||||
Description | When using the //@ annotations, a comment at the end that has an unmatched ' or " causes the kernel to report an error. | ||||||||||||
Steps To Reproduce | create file comment_parse.c: void f(){ //@assert \true;// Validates in 0'0" } Run: frama-c -cpp-command 'gcc -C -E' -pp-annot comment_parse.c Receive output: [kernel] preprocessing with "gcc -C -E -dD comment_parse.c" "comment_parse.c":5:[kernel] user error: Can't preprocess annotation: eof while parsing a char literal Annotation will be kept as is comment_parse.c:3:[kernel] user error: syntax error [kernel] user error: skipping file "comment_parse.c" that has errors. [kernel] Frama-C aborted: invalid user input. Removing the ' and " characters will cause no error to occur. | ||||||||||||
Tags | No tags attached. | ||||||||||||
Attached Files |
|