Frama-C Bug Tracking System - Frama-C
View Issue Details
0002307Frama-CKernelpublic2017-05-30 11:202017-05-31 15:14
evdenis 
virgile 
normalminoralways
assignedopen 
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
https://bts.frama-c.com/file_download.php?file_id=1186&type=bug
c test1.c (179) 2017-05-31 15:01
https://bts.frama-c.com/file_download.php?file_id=1187&type=bug
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

Notes
(0006400)
yakobowski   
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.
(0006402)
evdenis   
2017-05-31 15:00   
It's a part of specification generated by RTE plugin for function seq_show_option http://elixir.free-electrons.com/linux/v4.2.8/source/include/linux/seq_file.h#L158 [^]
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?
(0006404)
yakobowski   
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.