ghost_multiline_annot.2.res.oracle

[kernel] Parsing ghost_multiline_annot.c (with preprocessing)
[kernel] ghost_multiline_annot.c:48: 
  This kind of annotation is valid only inside ghost code:
  Location: between lines 48 and 49, before or at token: /@
  46    #ifdef P2
  47    int main()
  
  48    {
  49      /@ assert 2 == 2; @/
  
  50      return 0;
  51    }
[kernel] Frama-C aborted: invalid user input.