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] How to obtain a base variable's original variable?

  • Subject: [Frama-c-discuss] How to obtain a base variable's original variable?
  • From: abiao.yang at gmail.com (David Yang)
  • Date: Fri, 13 Sep 2013 17:16:07 +0800
Dear all,

First of all, my question is: How to obtain a Base.t variable's original
variable?

A Base(the Base module in frama-c api) variable can be like this:
WELL_next_0_S_next_0_S_next_0_S_chain
And it's original variable is a struct pointer: chain

I using Db.Outputs module to obtain the out-external variables of a
corresponding kernel function by using : val get_internal :
(Cil_types.kernel_function -> t) ref

The outputs obtained by val Db.Outputs.get_external has type:
Locations.Zone.t

I can iterate each variables by using :  Locations.Zone.map_i : (Base.t ->
Lattice_Interval_Set.Int_Intervals.t -> t) -> t -> t

e.g:

For debugging, I output each base.t :
WELL_next_0_S_next_0_S_next_0_S_chain
WELL_name_0_S_next_0_S_next_0_S_chain
WELL_file_0_S_next_0_S_next_0_S_chain
WELL_next_1_S_next_0_S_next_0_S_chain
WELL_name_1_S_next_0_S_next_0_S_chain
WELL_file_1_S_next_0_S_next_0_S_chain
....

I can see that this six base.t variables are derived from a struct pointer
named: chain

How can I get the base variable's original variable programmatically, not
by string expression matching ?

Looking forward to hearing from you.
Thanks for your attentions.

Best regards.
David Yang
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130913/e545d649/attachment.html>