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


  • Subject: [Frama-c-discuss] Modifying the AST to insert statements / declarations
  • From: Pierre.Karpman at rennes.supelec.fr (Pierre Karpman)
  • Date: Mon, 26 Mar 2012 11:23:27 +0200

Hello,

I have a piece of code that modifies the AST quite well now, but it 
gives rise to two comments/questions.

-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?

-In my instrumentation, I want (need) to declare temporary variables at 
the block level and be able to use these variables right after in the 
new instructions I'm creating. There doesn't seem to be an easy way to 
do this and what I'm doing now is more of a dirty hack:
     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.
     Now this seems to work sometimes, but it fairly regularly fails to 
add the variable declarations in the blocks. What's odd is that it seems 
to fail when other local declarations are missing, like e.g. in the case 
highlighted in bug report #1113.
     So I'm not sure if my hack *should* work all the time and doesn't 
because of a more complex issue, or if I'm just lucky that it works 
sometimes but really shouldn't (and then I would need to do the 
declarations in some other way)?

Cheers,
Pierre