--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on March 2012 ---
Hello, 2012/3/16 Pierre Karpman <Pierre.Karpman at rennes.supelec.fr>: > 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...> > > 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). A visitor is indeed the way to go. Basically, you have two choices: either you first create your own project using Visitor.frama_c_plain_copy, and use an inplace visitor inside the project, or you use directly a copy visitor that will do the copy and the transformation in one pass. The latter is more involved, especially if you want to generate local variables (they have to be bound to elements of the new project, i.e. fundec and local block, the latter not being readily available at this point), thus I would suggest to go with the former, at least for a first stage. The attached script contains a very basic visitor that generates a new local variable each time it encounters a block, initializes the variable to 0, and increments it at each call occurring inside the block. It does not use vstmt_aux, but vinstr, as the latter can return a list of instruction, while you can only transform a statement in another statement. If you're only interested in calls, that are instructions, this should be sufficient. If you really need to operate at statement level, just transform your initial statement into a block containing the new list of statements. Note that since the visitor operates on a new project named count_call, if you want to print its result, you have to launch frama-c like that: frama-c -load-script insert_stmt.ml file.c -then-on count_call -print Best regards, -- E tutto per oggi, a la prossima volta Virgile -------------- section suivante -------------- Une pi?ce jointe autre que texte a ?t? nettoy?e... Nom: insert_stmt.ml Type: text/x-ocaml Taille: 1589 octets Desc: non disponible URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120316/f1099e83/attachment.bin>