Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Replacing the CIL parser thru a plugin?

2012/2/15 Basile Starynkevitch <basile at starynkevitch.net>:

> Actually, I was told to write a GCC MELT extension (see http://gcc-melt.org/
> for more) to "inject" Gimple (and other GCC internal representations) into
> Frama-C. My initial thought was to produce, by a MELT extension, some JSON
> (or perhaps YAML or something else) representing as precisely as possible
> the Gimple internal representation of GCC in textual format, and have a
> small Frama-C plugin in Ocaml loading that format. I need to have separate

That seems reasonable. IIRC, there are some ocaml libraries to parse
json and possibly yaml (can't give pointers right away , though)

>> You can use the File.add_new_file_type.
>
> Sorry, but where can I find that function? I'm grepping the whole
> So I guess you mean File.new_file_type

Yes, this is the right name. Sorry for the typo.

>
> I might use ".json" as suffix if I decide to generate JSON.
> (I won't use ".melt" because ".melt" is reserverd for MELT source files)
>

That's fine, you can use any suffix you see fit. The only minor
inconvenience I see would be that
it's a bit too generic, in the sense that it'd prevent an hypothetical
other plug-in similar to yours
but with another front-end to use .json suffix. But we can delay this
discussion until such a plugin exists.

>
> So I'm understanding that Frama-C needs two related internal representations describing a single C source code.
>

Yes and No. The main representation is Cil_types.file. Almost all
plugins, and all plugins doing semantical analyses operate on this
AST.
Cabs.file is what is normally produced by the frontc parser. It is
closer to the original file, and that's why some plugins performing
syntactic checks use it.
For instance, there's no point for a plugin that checks if all
functions have exactly one return statement to operate on
Cil_types.file, since this is ensured
in the elaboration phase. Such a plugin must rely on Cabs.file, where
it will access to the statements as they have been written.
This is the reason why we keep Cabs.file. However, it is not mandatory
to have this Cabs.file to use Frama-C. In fact, this Cabs.file does
not copied in projects that are created as the result of code
transformation (e.g. slicing) that operate at the Cil_types.file
level.

>
> Is there any mean to check that the two representations fits nicely together..?
>

No. The only possibility is to generate a Cabs.file and use
Cabs2cil.convFile on it.

> (Or maybe I didn't understood your remark about Cabs2cil.convFile; should a newbie use it or not?)

I'd say that it's easier than creating directly a Cil_types.file. The
AST has quite a lot of sharing and some intricate invariants, and it
would be difficult to get them right. Cabs.file is far easier to
grasp. That said, if gimple is close enough from Cil_types.file, the
direct creation might make sense (rather than having a second
elaboration phase after the one of gcc).

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile