--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on March 2012 ---
[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