--- layout: fc_discuss_archives title: Message 3 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,
  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