--- layout: fc_discuss_archives title: Message 96 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?



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