--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on April 2011 ---
Hello, You can use: FC_file.pretty_ast ~prj:project (); That print the C file on the stdout. The kernel option: -ocode file.c or else: -then-on "your project name" -ocode file.c can be used for redirection to a file. Patrick. -- Patrick Baudin, CEA, LIST, DILS, F-91191 Gif-sur-Yvette cedex, France. tel: +33 (0)1 6908 2072 > Hello! > > 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? > > Thank you. > > Zakaria Chihani. > > > PS : Here's a little summary of what was done. Just in case we did > something wrong :? > > We take a .c file. We " File.create_project_from_visitor" using a > class "cost" that inherits from generic_frama_c_visitor. > Using the AST from the Cil_types.mli, we redefine vglob_aux to go > through all the GFun, and retrieve the body, which we visit. > That visit gives us a cost = k. > We then add an annotation above the function (in the post_cond of a > behavior, added to the behavior list in the funspec, in the fundec, in > the GFun) saying that the new cost must be less or equal to the old > cost plus the obtained k. (this is, of course, an "ensure" clause ) > > Thus we create a relation predicate [1], then put it in an IDed > predicate, then add the couple (termination = Normal, our predicate) > to the post_cond of a behavior, which we add all the way up to the GFun. > > At the end, we simply use the > ChangeDoChildrenPost([annotatedFun],fun x -> x) > visitAction, and a > | _ -> JustCopy > otherwise. > > 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? > > > > [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. > > How can we set up the lv_id? Having no options, we used > Logic_const.fresh_term_id (); is that okay? > > Thank you so much for your help. > > > > ------------------------------------------------------------------------ > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss