--- layout: fc_discuss_archives title: Message 92 from Frama-C-discuss on September 2013 ---
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>