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

[Frama-c-discuss] Problem with ChangeDoChildrenPost



Hello! Me again!

Right, so everything works, thank you so much for your help!
But when we use 
? Cil.d_global Format.std_formatter annotatedFun ;
It prints, on the std_out, exactly what we want, the ensure clause is right where we need it.

But there's nothing in the outed file, it doesn't change the GFun nodes into Annotated GFun nodes (adding an ensure clause).
The colored parts are of interest...
___________________________________________
? method vglob_aux g=
??? begin match g with
????? | GFun (oldFundec,location1) ->
????? (*...other things here...*)
??? ? let newFundec = ??? ?? 
??? ??? {oldFundec with sspec = newSpecc} in
??? ? let annotatedFun = GFun (newFundec,location1)
??? ? in 
??? ?? Cil.d_global Format.std_formatter annotatedFun ; (*shows an annotated fun*)
???? (*? ChangeDoChildrenPost ( [annotatedFun], fun x -> x)? didn't work either*)
??? ?? ChangeToPost( [annotatedFun], fun x -> x)???? (*Doesn't seem to be working...*)
????? | _ ->? JustCopy
??? end
?____________________________________________ ??? 

In case ChangeToPost wasn't the problem, here's how we do the copy afterwards,
In another .ml, we apply CerCo, it passes to cost, here, a Cabs.file, the name of the incrementation function, and the global var to be incremented.

So we need to change the current Project, to have the CerCo_transformation as current Project.
_________________________________________________
let cost ((fname, _) as file, cost_id, cost_incr) =
? let annotatedFile =??? 
??? Parameters.Files.set [fname];
??? File.init_from_cmdline ();
??? File.create_project_from_visitor 
????? "cerCo_Annotated" 
????? (new cost cost_incr cost_id)
? in 
??? Project.on
????? annotatedFile
?????? (fun _ ->
?????? Parameters.CodeOutput.set "tests/_Pluginnned.c";
?????? File.pretty_ast ())
???? ();
annotatedFile
___________________________________________________

NB: The only changed nodes are the GFun, and the only thing changing in them is the behavior (post_cond)


Thank you so much for your help...We were lost without you.

Zakaria Chihani.





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