--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on April 2011 ---
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