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 13:28:38 +0200
Hello,
> >/  -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 ;-)
Okay, so I'll probably do a copy again :)
>
> >/      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.
I'm not sure I understand what you mean about vcurrent_block. I'd 
already tried saving the value of the current block while in the vblock 
visitor (say in "cbk"), and then making the declarations in vinst as:

     let vi = makeLocalVar (Extlib.the self#current_func) ~scope:cbk 
vi_name vi_type

but this doesn't work (the varinfo's created fine and I can use it to 
create new instructions that are using it, but the variable declaration 
itself is not inserted at the beginning of the block as it should). Is 
that what you were suggesting?

Anyway I was wondering if something could be done by visiting at the 
statement level and creating a new block around the part of code I'm 
modifying; maybe the variable insertion will work "better" in this case?
> However, your approach
> should work too, even though it's difficult to say more without seeing
> the code.
I'll check with my supervisors, but I can probably make the code 
available somewhere (I think it's supposed to be open-source and all).

Cheers,
Pierre
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120326/6121ca1e/attachment.html>