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?

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} ***