--- layout: fc_discuss_archives title: Message 21 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,

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