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

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>