--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on July 2012 ---
Hello Virgile, 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? 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? If this works, can I just call Visitor.visitFramacFile (new Plugin.plugin) (Ast.get ()); twice with the corresponding options for each pass? -- Best regards, Boris (Message sent again because yesterday's message didn't arrive)