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] Modifying the AST to insert statements / declarations

Hello,

2012/3/26 Pierre Karpman <Pierre.Karpman at rennes.supelec.fr>:

> -My code doesn't do any analysis whatsoever after the instrumentation I do
> in the AST, so I'm not sure that doing the modifications on a new AST from a
> new project is necessary. From the small examples I've been using, it really
> seems okay to modify the original AST (on which the analysis's been
> performed) in place, but I'm not sure it's not only because I've been
> (un)lucky with my examples?

The point about project is not what your analysis itself does, but
what other plug-ins have done or will do after yours. There might be
subtle interactions between them, and you don't really want to debug
that ;-)

> ? ?I'm using the vinst and vblock visitors; if I use Cil.makeLocalVar in
> vinst only, the variable is never actually put in the block declarations (at
> least not with any of the parameters I tried for this function), so I create
> a placeholder in vinst by using Cil.makeVarinfo, and I maintain a stack of
> variables to declare, and do all the corresponding makeLocalVar calls in the
> "post" function of vblock (using ChangeDoChildrenPost), which otherwise does
> nothing.

Admittedly, there ought to be a vcurrent_block on the model of
vcurrent_kf and the like (that you can emulate fairly easily though),
so that you can use it in
makeLocalVar in vinst, without any post_action. However, your approach
should work too, even though it's difficult to say more without seeing
the code.

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