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

[Frama-c-discuss] Inserting global annotation into the AST



Hello,

2012/3/20 Boris Hollas <hollas at informatik.htw-dresden.de>:
> I want to define global annotations that are associated to functions and
> insert these into the AST. I use an inplace visitor and I want to
> generate the global annotations in method vfunc, as they are associated
> to the function being visited. I assume that I can't insert these
> annotations by overriding vglob_aux as vglob_aux wouldn't be invoked if
> there were no globals in the original source. Also, I want the global
> annotations the be inserted before the function definition.

If you have a function, there is necessarily a GFun _ global
somewhere. Thus, you can use vglob_aux to add new globals before the
function, e.g. with
a list that is filled when visiting the fundec and used in a
post-action via ChangeDoChildrenPost in vglob_aux.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile