Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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