--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on July 2012 ---
Hello, 2012/7/10 Boris Hollas <hollas at informatik.htw-dresden.de>: > yes, I have to inspect the original source to declare appropriate > globals and loc1 and loc2 are in the same file. Can I solve the problem > by two-pass parsing? > A first pass with Kernel.ReadAnnot.Off () generates the globals and > writes them to a file defs.h with Cil.d_global. In this case, how do I > change Cil.defaultCilPrinter to my out_channel? Yes, this should work. I'm not sure I understand your question, though: Cil.d_global, as all pretty-printing functions, takes as first argument a formatter channel, that you can create from an out_channel with Format.formatter_of_out_channel (see OCaml's standard library manual for more information). > Then a second pass can include defs.h with Kernel.CppExtraArgs and do > any further processing. However, the pretty-printed globals may contain > non-ASCII symbols. Can the toolchain handle these? In theory yes. If there is some issue, you can switch to -no-unicode pretty-printing (after having reported the problem of course ;-) > If this works, can I just call > Visitor.visitFramacFile (new Plugin.plugin) (Ast.get ()); > twice with the corresponding options for each pass? I would suggest that you use distinct projects (possibly removing the old one after everything is processed) for the two phases. Best regards, -- E tutto per oggi, a la prossima volta Virgile