--- layout: fc_discuss_archives title: Message 96 from Frama-C-discuss on September 2013 ---
Hi, This information does not currently exist programatically. A slight modification of the file src/value/initial_state.ml should do the trick, if you feel motivated; as a bonus point, you would obtain a full l-value, and not just the base variable. Alternatively, you can have a look at the field vdescr of the varinfo underlying the base. This should be easier to parse than the name of the base. On Fri, Sep 13, 2013 at 11:16 AM, David Yang <abiao.yang at gmail.com> wrote: > > 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 > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -- Boris