--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on July 2012 ---
Hello Boris, 2012/7/9 Boris Hollas <hollas at informatik.htw-dresden.de>: > my plugin inserts globals into the AST using an inplace-vistor and > Cil.ChangeDoChildrenPost in vglob_aux. I want these globals to be > accessible to the user in the source code. For example, if the global is > inserted in loc1, I want the user to be able to use this global in loc2 > if loc1 < loc2. Right now, Frama-C reports an error at loc2 because the > global is yet undefined at parse time. Is there a way to defer parsing > loc2 until loc1 has been parsed and the global been inserted? No, it's not possible right away. If the new globals can be declared independently from the source code under analysis, the easiest thing to do is to define an header file with them, possibly adding "-include plugin_extra_decl.h" to -cpp-extra-args options if you don't want to force the user to add an #include directive on all his files (Note however that this is not a perfect solution, as the user still has to be aware that all the files must end in .c, even if they have been already pre-processed, otherwise, the -include won't be used). If you need to inspect the original source to declare appropriate globals, it'd still be possible to use a variant of this method when loc1 and loc2 are in two distinct files: first parse file1, generate your globals, and print the resulting code, then create a new project with file2 as input file and "-include file1_pretty_printed.c" as cpp-extra-args. If loc1 and loc2 are in the same file, there's no way to stop parsing and type-checking in the middle of a file. Best regards, -- E tutto per oggi, a la prossima volta Virgile