--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on April 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Plugin development : saving a project in a readable format



Hello,

Le 04/04/2011 22:57, zakaria chihani a ?crit :
> We are designing a frama-c plug-in for CerCo.
> We found inspiration in the example given on page 67 of the plug-in
> development guide, adding zero_division assertions.
> The example creates a project after adding assertions to a copy of the
> original. so the result is a Project.t
>
> We need to save that project into .c file, and can't find, in the
> Project.mli or the Cil.mli, or File.ml...
> Project.save doesn't work, it doesn't save in a readable format.
>
> How can we get the .c file from the project?

As Patrick said, File.pretty_ast is your friend. You have to give as 
argument your project and a formatter corresponding to the file you want 
to create (or to set option -ocode programatically).

More generally, you can use Project.set_current (resp. Project.on) to 
change the current project globally (resp. locally): then any function 
is applied on the given project.

Here is a small exemple which duplicates the current project and pretty 
print the AST of the new project in "my_file.i".

===
let main () =
   let prj =
     (* just duplicate the current project *)
     File.create_project_from_visitor
       "my_project"
       (fun prj -> new Visitor.frama_c_copy prj)
   in
   Project.on
     prj
     (fun p ->
       Parameters.CodeOutput.set "my_file.i";
       (* no argument given to File.pretty_ast:
          implicitely printed the AST of project [prj]
          into file "my_file.i". *)
       File.pretty_ast ())
     ()

let () = Db.Main.extend main
===

> We tried without putting the annotatedFun in a list, it resulted in an
> error, and we cannot figure out why.
> The guide says that the visit action replaces the node with the given
> node. the GFun we matched upon was a node, annotatedFun is a node,
> [annotatedFun] is a list. Why is that?

The guide is right for most nodes, but there is at least one exception ;-).

The method vglob_aux has type global -> global list Cil.visitAction. 
Thus you are to put a list. The reason is that you might insert some new 
globals into the AST.

Do not hesitate to have a look at the kernel API 
(http://frama-c.com/download/frama-c-Carbon-20110201_api.tar.gz) to get 
the exact expected type of a function.

> [1] For this, we use Logic_const.tvar which takes, at some point, a
> logic_var.
>
> and logic_var = {
> mutable lv_name : string; (** name of the variable. *)
> mutable lv_id : int; (** unique identifier *)
> mutable lv_type : logic_type; (** type of the variable. *)
> mutable lv_origin : varinfo option (** when the logic variable stems from a
> C variable, set to the original C variable.
> *)
> }
>
> At some point in the commented area over the identified_term type, in
> the Cil_types.mli, we read
> Use [Logic_const.new_location] to generate a new id. *)
> But this method isn't in the Logic_const module, nor anywhere else in
> the source of the Carbon version.

That is a documentation error which can be reported to our BTS 
(bts.frama-c.com).

> How can we set up the lv_id? Having no options, we used
> Logic_const.fresh_term_id (); is that okay?

Not really: that not the expected counter there.

The simplest way to create a new logic variable is to call function 
Cil_const.make_logic_var and let it to choose a valid id.

Smart constructors for AST nodes are in one of the following modules: 
Cil, Cil_const, Logic_const or Logic_utils. I agree that it is not 
always easy to find what you are searching in the API.

Hope this helps,
Julien Signoles
-- 
Ing?nieur-Chercheur
CEA LIST, Laboratoire de S?ret? des Logiciels
point courrier 94, 91191 Gif-Sur-Yvette Cedex
tel:(+33)1.69.08.71.82  fax:(+33)1.69.08.83.95  Julien.Signoles at cea.fr