preprocessor fail: unterminated comment
ID0002307: This issue was created automatically from Mantis Issue 2307. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002307 | Frama-C | Kernel | public | 2017-05-30 | 2017-05-31 |
| Reporter | evdenis | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C 14-Silicon | Target Version | - | Fixed in Version | - |
Description :
Gcc compiles this code, but frama-c throws preprocessor error. $ gcc -w -c rte.c $ echo $? 0
Code: const char seq_show_option_value; void kmalloc_node_tmp; __inline static void seq_show_option() { const char * name = 0; int * m = 0; /@ behavior pre_seq_escape: assigns *m \from *("= \t\n\"+0), *(name+0), *m; / &seq_show_option_value; } __inline static void mem_cgroup_update_page_stat() { asm volatile ( ".pushsection __bug_table"a"\n.popsection": : "i"("/lib/modules/4.8.12300.fc25.x86_64/build/include/linux/memcontrol.h"), "i"(sizeof( int))) /@ assert \false; */ ; } void kmalloc_node() { kmalloc_node_tmp = kmalloc(); }
Error: [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing rte.c (with preprocessing) rte.c:17:7: error: unterminated comment /*@ assert \false; */ ; ^ "rte.c":23:[kernel] user error: Can't preprocess annotation: Preprocessor call exited with an error Some annotations will be kept as is
Steps To Reproduce :
frama-c rte.c