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: Julien.Signoles at cea.fr (Julien Signoles)
  • Date: Fri, 16 Mar 2012 12:45:15 +0100
  • In-reply-to: <CA+yPOVg_rWHNfGDd_sji+MMfU6G=X8qEYPO0w27ou=5AJoeRpA@mail.gmail.com>
  • References: <4F62F793.9090807@rennes.supelec.fr> <CA+yPOVg_rWHNfGDd_sji+MMfU6G=X8qEYPO0w27ou=5AJoeRpA@mail.gmail.com>
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