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] Problem with ChangeDoChildrenPost

  • Subject: [Frama-c-discuss] Problem with ChangeDoChildrenPost
  • From: uaz11 at yahoo.fr (zakaria chihani)
  • Date: Thu, 7 Apr 2011 00:58:48 +0100 (BST)
  • In-reply-to: <mailman.69.1301565700.30458.frama-c-discuss@lists.gforge.inria.fr>
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>