--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on April 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with the ChangeDoChildrenPost (bis)



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>