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: virgile.prevosto at m4x.org (Virgile Prevosto)
- Date: Fri, 16 Mar 2012 11:07:08 +0100
- In-reply-to: <4F62F793.9090807@rennes.supelec.fr>
- References: <4F62F793.9090807@rennes.supelec.fr>
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>
- Follow-Ups:
- [Frama-c-discuss] Modifying the AST to insert statements / declarations
- From: virgile.prevosto at m4x.org (Virgile Prevosto)
- [Frama-c-discuss] Modifying the AST to insert statements / declarations
- From: Julien.Signoles at cea.fr (Julien Signoles)
- [Frama-c-discuss] Modifying the AST to insert statements / declarations
- References:
- [Frama-c-discuss] Modifying the AST to insert statements / declarations
- From: Pierre.Karpman at rennes.supelec.fr (Pierre Karpman)
- [Frama-c-discuss] Modifying the AST to insert statements / declarations
- Prev by Date: [Frama-c-discuss] Modifying the AST to insert statements / declarations
- Next by Date: [Frama-c-discuss] Modifying the AST to insert statements / declarations
- Previous by thread: [Frama-c-discuss] Modifying the AST to insert statements / declarations
- Next by thread: [Frama-c-discuss] Modifying the AST to insert statements / declarations
- Index(es):