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] Using generated globals in the source code

  • Subject: [Frama-c-discuss] Using generated globals in the source code
  • From: hollas at informatik.htw-dresden.de (Boris Hollas)
  • Date: Mon, 09 Jul 2012 08:18:31 +0200
Hello,

my plugin inserts globals into the AST using an inplace-vistor and
Cil.ChangeDoChildrenPost in vglob_aux. I want these globals to be
accessible to the user in the source code. For example, if the global is
inserted in loc1, I want the user to be able to use this global in loc2
if loc1 < loc2. Right now, Frama-C reports an error at loc2 because the
global is yet undefined at parse time. Is there a way to defer parsing
loc2 until loc1 has been parsed and the global been inserted?
-- 
Best regards,
Boris