--- layout: fc_discuss_archives title: Message 65 from Frama-C-discuss on February 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



On Wed, Feb 15, 2012 at 10:21:12AM +0100, Virgile Prevosto wrote:
> Hello Basile,
> 
> 2012/2/8 Basile Starynkevitch <basile at starynkevitch.net>:
> 
> > Imagine I have some intermediate representation of C-like or Fortran-like
> > souece code, in e.g. some JSON or YAML file -in a format I can define and
> > enhance, which is produced by some generator-, and I want to code in Ocaml a
> > plugin to construct in Frama-C's memory a representation of it, probably by
> > calling suitable constructors from cil/src/cil_types.mli, how should I
> > proceed?
> >

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
processes since I definitely do not want to link MELT inside Frama-C,
because mixing three different garbage collector (the one from GCC, the MELT
one above the GCC one, and the Ocaml one) is not reasonable.

> 
> You can use the File.add_new_file_type.

Sorry, but where can I find that function? I'm grepping the whole
frama-c-Nitrogen-20111001/ and I can't find any add_new_file_type function.
I can't find it in the frama-c-base package of my Debian/Sid.

And the frama-c-Nitrogen-20111001/src/kernel/file.mli interface file don't mention it.

However, it contains 

val new_file_type:
  string -> (string -> Cil_types.file * Cabs.file) -> unit
  (** [new_file_type suffix func funcname] registers a new type of files (with
      corresponding suffix) as recognized by Frama-C through [func]. *)

So I guess you mean File.new_file_type


> This function takes two
> arguments: a suffix identifying the files that have
> to be treated by the external parser (say .melt for instance), and a
> function taking a filename and returning a pair (Cil_types.file *
> Cabs.file), 

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 is a normalized AST and an untyped AST. Depending on your
> representation, It is of course possible to directly generate the
> normalized AST (possibly using a dummy Cabs.file: it is only used by
> plug-ins that  depend on the exact form of the code rather than on its
> semantics),  but in order to ensure that all invariants expected by CIL on
> the AST  are met, generating an untyped AST (Cabs.fil) and converting it 
> through Cabs2cil.convFile seems the easiest way.

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

The files frama-c-Nitrogen-20111001/cil/src/frontc/cabs.ml &
frama-c-Nitrogen-20111001/cil/src/cil_types.mli seems to represent similar
things.

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

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

Thanks for your kind reply.

Cheers.

-- 
Basile STARYNKEVITCH         http://starynkevitch.net/Basile/
email: basile<at>starynkevitch<dot>net mobile: +33 6 8501 2359
8, rue de la Faiencerie, 92340 Bourg La Reine, France
*** opinions {are only mines, sont seulement les miennes} ***