--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on March 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Modifying the AST to insert statements / declarations



Hello,

On 03/16/2012 11:07 AM, Virgile Prevosto wrote:
> 2012/3/16 Pierre Karpman<Pierre.Karpman at rennes.supelec.fr>:
> 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.

Virgile is right.

But if you want an example of the latter, i.e. a copy visitor in one 
pass which generates local variable, you may have a look at plug-in 
E-ACSL available here: http://frama-c.com/eacsl.html. The implementation 
is however more complicated than the script in the Virgile's mail.

--
Julien