--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on April 2011 ---
Hello! We overrode vspec as you advised, and we didn't do vglob_aux, because we don't actually change the function body (yet) we just process the body of the function (with a self-made method) so we just call it with the fundec returned by the self#current_func. We print the result with the cil.d_funspec, but we still don't get it on the outed file. ?method vspec spec= ??? begin match self#current_func with ????? |Some fdec? -> ?????????? (*? extractCostFrom fdec.sbody.bstmts ; ?????????? create a new spec with adding the spec_behavior : newSpecc ????????? *) ??? ?? Cil.d_funspec Format.std_formatter newSpecc ; (*prints well*) ??? ?? ChangeDoChildrenPost(newSpecc,fun x -> x) (*doesn't show*) ????? | _ -> JustCopy ??? end So maybe it's a problem with the way we out the file, but we can't figure out where... Here's what we do : let cost ((fname, _) as file, cost_id, cost_incr) = (*(fname,_) is a Cabs.file that we passed to CerCo earlier, now we create a new project with its name*) ? let annotatedFile =??? ??? Parameters.Files.set [fname]; ??? File.init_from_cmdline (); ??? File.create_project_from_visitor ????? "cerCo_Annotated" ????? (new cost cost_incr cost_id) ?????????????????????? (*? inherits from? Visitor.generic_frama_c_visitor prj (Cil.copy_visit())? *) ? in ??? Project.on ????? annotatedFile ?????? (fun _ -> ?????? Parameters.CodeOutput.set "tests/_out.c"; ?????? File.pretty_ast ()) ???? (); annotatedFile Thank you so much for your time. H. Zakaria Chihani. PS : here's to keep track ;) Message: 6 Date: Mon, 11 Apr 2011 15:58:20 +0200 From: Virgile Prevosto <virgile.prevosto at cea.fr> Subject: Re: [Frama-c-discuss] Difference between Kernel_function and ??? GFun node To: frama-c-discuss at lists.gforge.inria.fr Message-ID: <20110411155820.676d940a at is010235> Content-Type: text/plain; charset=ISO-8859-1 Le lun. 11 avril 2011 10:46:38 CEST, zakaria chihani <uaz11 at yahoo.fr> a ?crit : > I can't understand the difference between the GFun node and the kernel_function. sspec can't be completely irrelevant, I presume. Well, for most practical purposes, sspec is irrelevant. It is only used in freshly type-checked AST, until Frama-C's internal tables are properly filled. It's not a stage where plug-ins intervene much (in fact, there isn't any hook to do so). > The only thing changing is indeed the vspec, but it changes with regards to what is in the function itself, we need to process the body (with vglob_aux) in order to get "what to put" in the postcondition (with vspec). OK, then you're right, it makes sense to use vglob_aux to do that. > > So we need to also override vglob_aux. > The thing is, we don't know the specific order in which these two (vglob_aux and vspec) are gonna be called. the spec is somehow a child of the function, thus vspec is called after vglob_aux (on the other hand, an action in ChangeDoChildrenPost for vspec will be performed before an action in ChangeDoChildrenPost for vglob_aux) > Isn't there an easier way to use Visitor.current_kf and set_current_kf, to link the generated GFun node, with the associated kernel_function? Unfortunately no: current_kf always refer to original function being visited. In fact, since the visitor can return more than one global (or for that matter, to turn a decl into def or vice-versa), it is not really possible to have a current_kf for the new function in the general case. Only the original one is meaningful. -- Virgile Prevosto Ing?nieur-Chercheur, CEA, LIST Laboratoire de S?ret? des Logiciels +33/0 1 69 08 82 98 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110414/143f7cb1/attachment.htm>