--- layout: fc_discuss_archives title: Message 92 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] How to obtain a base variable's original variable?



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>