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: Fri, 16 Mar 2012 09:19:31 +0100
Hello,

I'm trying to see how it is possible to modify a Cil AST to insert "new 
code" in the source that's being processed.
More precisely, from a statement like e.g.

funk(a, b, c);

I'd like to get something like

<some statements generated by my plugin>
<some local variable declarations...>
funk(a,b,c);
<some statements...>

The plugin I'm working currently does code insertion by simply printing 
out a patch, but this doesn't quite seem to work for post-call 
statements in some cases.
So, that's why I'd like to do all those inserts directly in the AST 
(pretty much in the way Frama-C currently expands some pieces of code I 
guess?), so that I could get the modified code by doing something like 
"frama-c -meplugin -print somecode.c".

Now I'm not sure how to do that properly (hence this email): I 
considered doing the modifications by redefining a vstmt_aux in a 
generic visitor, but I'm not sure this should work (I did a quick few 
tests, and it doesn't seem that inserting new statements will have them 
printed by frama-c, although they're taken into account by the 
subsequent analysis done on the AST).

Can someone give me pointers to where this sort of code exists in 
Frama-C or to how to do this thing properly?

Cheers,
Pierre