Why does not VeriFast use CIL parser?

[necto]

Hello,
Recently I've discovered a very interesting project: https://github.com/cil-project/cil
I wonder why does VeriFast use its own C parser over the CIL one.

CIL seems to be a mature project. Also, given that Frama-C is based on it, it should not be difficult to make it support VeriFast annotations (Frama-C uses ACSL that exploits /*@ @*/ and //@ comment syntax).

At the same time VeriFast parser has some obscure pecularities (e.g. #26, #16, #38, #41).

The only reason for not using it I come up with is the support for Java language. But IMHO it does not hurt to have separate parsers for two different languages.

Is there any reason (except of the obvious porting effort) to not replace the current parser with CIL?

[btj]

We (actually, Jan Smans) made an attempt to put CIL in front of VeriFast some years ago, and it failed. If I remember correctly, a main reason was that comments were not retained. That still seems to be the case, judging by http:https://cil-project.github.io/cil/doc/html/cil/cil011.html .

But you're right, Frama-C seems to have solved this problem. I had a peek into the Frama-C source code, and it seems they're using a patched version of CIL that does retain comments.

Another problem is this: we would like to have precise source locations, including column numbers, for all program elements. CIL requires that you first run a C preprocessor on the source code, which in general may mess up the column numbers (if the line contains a macro that expands to something of a different width).

But that might be a sufficiently unimportant problem that such a frontend would still be useful. We should probably have another go at this.

In the meantime, if you are particularly annoyed by some parsing issue, do report it.

[master-q]

Totally, I think we should port libclang parser onto VeriFast. I need some time to do that...

[master-q]

I tried to use clang to pick up comment. But it only find global comment...

$ cat hello.c
// Comment in global
int main() {
  /* Comment in function */
  return 1+2;
}
$ clang -Xclang -ast-dump -fsyntax-only -fparse-all-comments hello.c
TranslationUnitDecl 0xfa48014d80 <<invalid sloc>> <invalid sloc>
|-TypedefDecl 0xfa48015278 <<invalid sloc>> <invalid sloc> implicit __int128_t '__int128'
| `-BuiltinType 0xfa48014fd0 '__int128'
|-TypedefDecl 0xfa480152d8 <<invalid sloc>> <invalid sloc> implicit __uint128_t 'unsigned __int128'
| `-BuiltinType 0xfa48014ff0 'unsigned __int128'
|-TypedefDecl 0xfa48015368 <<invalid sloc>> <invalid sloc> implicit __builtin_ms_va_list 'char *'
| `-PointerType 0xfa48015330 'char *'
|   `-BuiltinType 0xfa48014e10 'char'
|-TypedefDecl 0xfa48015618 <<invalid sloc>> <invalid sloc> implicit __builtin_va_list 'struct __va_list_tag [1]'
| `-ConstantArrayType 0xfa480155c0 'struct __va_list_tag [1]' 1 
|   `-RecordType 0xfa48015440 'struct __va_list_tag'
|     `-Record 0xfa480153b8 '__va_list_tag'
`-FunctionDecl 0xfa480156e8 <hello.c:2:1, line:5:1> line:2:5 main 'int ()'
  |-CompoundStmt 0xfa48015878 <col:12, line:5:1>
  | `-ReturnStmt 0xfa48015860 <line:4:3, col:12>
  |   `-BinaryOperator 0xfa48015838 <col:10, col:12> 'int' '+'
  |     |-IntegerLiteral 0xfa480157f8 <col:10> 'int' 1
  |     `-IntegerLiteral 0xfa48015818 <col:12> 'int' 2
  `-FullComment 0xfa48015940 <line:1:3, col:20>
    `-ParagraphComment 0xfa48015910 <col:3, col:20>
      `-TextComment 0xfa480158e0 <col:3, col:20> Text=" Comment in global"