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

  • Subject: [Frama-c-discuss] Plugin development : saving a project in a readable format
  • From: uaz11 at yahoo.fr (zakaria chihani)
  • Date: Mon, 4 Apr 2011 21:57:12 +0100 (BST)
  • In-reply-to: <mailman.67.1301479348.7162.frama-c-discuss@lists.gforge.inria.fr>
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.



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110404/5803f943/attachment.htm>