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] unbound value when calling "Annotations.get_annotations"

  • Subject: [Frama-c-discuss] unbound value when calling "Annotations.get_annotations"
  • From: njucslzh0714 at gmail.com (刘自恒)
  • Date: Wed, 20 Jul 2011 15:59:51 +0800
  • In-reply-to: <CALiiei79wZVZWh9mRLzRjsOZmGp3=BfpTOHv_Bn=o9LLmwNC8Q@mail.gmail.com>
  • References: <CALiiei4qQo5T2Xd2G3jBa+5CAwmG0zxHWOpTsLdZYH_HCJLEtA@mail.gmail.com> <CALiiei79wZVZWh9mRLzRjsOZmGp3=BfpTOHv_Bn=o9LLmwNC8Q@mail.gmail.com>
What I mean for "Is it allowed to add a new field to Cil_type.stmt" is that
can I extend it just like Registering a New Internal State.
Of course I can add the field directly to Cil_type.stmt which is a very very
bad method because it changes Frama-C kernel. Maybe the best way is to use
hash tables to store the extra information.

Sorry for not posting my own magic answer after resolving it.

Best Wishes.


Henry Liu.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110720/a5ad4db0/attachment.htm>