--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on April 2011 ---
Hello! Thank you for the other answer and sorry I didn't change the subject before sending this one, my bad... We overrode vspec as you advised, but we still don't get it on the outed file. We tried printing the result with the cil.d_funspec, which works perfectly... 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. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110415/9ec6e998/attachment.htm>