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] 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