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 the ChangeDoChildrenPost (bis)

  • Subject: [Frama-c-discuss] Problem with the ChangeDoChildrenPost (bis)
  • From: uaz11 at yahoo.fr (zakaria chihani)
  • Date: Fri, 15 Apr 2011 12:28:06 +0100 (BST)
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>