--- layout: fc_discuss_archives title: Message 65 from Frama-C-discuss on February 2012 ---
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} ***