--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on July 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Using generated globals in the source code



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