Frama-C Bug Tracking System - Frama-C
View Issue Details
0002307Frama-CKernelpublic2017-05-30 11:202017-05-31 15:14
Frama-C 14-Silicon 
0002307: preprocessor fail: unterminated comment
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
frama-c rte.c
No tags attached.
c rte.c (641) 2017-05-30 11:20
c test1.c (179) 2017-05-31 15:01
Issue History
2017-05-30 11:20evdenisNew Issue
2017-05-30 11:20evdenisFile Added: rte.c
2017-05-30 15:21yakobowskiNote Added: 0006400
2017-05-31 14:02signolesAssigned To => virgile
2017-05-31 14:02signolesStatusnew => assigned
2017-05-31 14:07signolesAssigned Tovirgile => yakobowski
2017-05-31 14:07signolesStatusassigned => feedback
2017-05-31 15:00evdenisNote Added: 0006402
2017-05-31 15:00evdenisStatusfeedback => assigned
2017-05-31 15:01evdenisFile Added: test1.c
2017-05-31 15:03virgileAssigned Toyakobowski => virgile
2017-05-31 15:14yakobowskiNote Added: 0006404

2017-05-30 15:21   
I do not understand the meaning of __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; */ ; } What does 'assert \false' means here? Did you mean __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; */ ; } (Additional ';' ?) If so, depending on the version of Frama-C used, you get a crash or an error. But all are actually unrelated to the asm clause, and are actually due to the strange from clause *("= \t\n\\"+0). This clause should be removed for at least two reasons: - you cannot really "depend" on something which is constant - constant strings have an identity in C, since equal but distinct constant strings may be different objects. Currently, support for this in ACSL is non-existent.
2017-05-31 15:00   
It's a part of specification generated by RTE plugin for function seq_show_option It's impossible to attach the whole example because its size is too big. I used Creduce to provide the example above. Example with more details: /*@ assigns *m; assigns *m \from *m, c; */ extern void seq_putc(struct seq_file *m, char c); /*@ assigns *m; assigns *m \from *m, *(s+(0 ..)), *(esc+(0 ..)); */ extern void seq_escape(struct seq_file *m, char const *s, char const *esc); __inline static void seq_show_option(struct seq_file *m, char const *name, char const *value) { /*@ behavior pre_seq_putc: assigns *m; assigns *m \from *m; */ seq_putc(m,(char)','); /*@ behavior pre_seq_escape: assigns *m; assigns *m \from *(",= \t\n\\"+(0 ..)), *(name+(0 ..)), *m; */ seq_escape(m,name,",= \t\n\\"); if (value) { /*@ behavior pre_seq_putc_2: assigns *m; assigns *m \from *m; */ seq_putc(m,(char)'='); /*@ behavior pre_seq_escape_2: assigns *m; assigns *m \from *(", \t\n\\"+(0 ..)), *(value+(0 ..)), *m; */ seq_escape(m,value,", \t\n\\"); } return; } Artificial example for RTE (test.c): extern void seq_escape(int *m, char const *s, char const *esc); void seq_show_option(int *m, char const *name, char const *value) { seq_escape(m,name,",= \t\n\\"); return; } $ frama-c -rte -rte-all -rte-precond -main seq_show_option ./test.c -then -print /* Generated by Frama-C */ /*@ assigns *m; assigns *m \from *m, *(s+(0 ..)), *(esc+(0 ..)); */ extern void seq_escape(int *m, char const *s, char const *esc); void seq_show_option(int *m, char const *name, char const *value) { /*@ behavior pre_seq_escape: assigns *m; assigns *m \from *(",= \t\n\\"+(0 ..)), *(name+(0 ..)), *m; */ seq_escape(m,name,",= \t\n\\"); return; } Maybe the issue can be categorized as RTE?
2017-05-31 15:14   
Very interesting, thanks. So the dubious 'from' clause is the specialization of the generic/inferred clause for 'seq_escape' for the particular call on ",= \t\n\\", by option -rte-precond. I'm not sure what the fix should be, but at least we have narrowed the problem.