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: boris at yakobowski.org (Boris Yakobowski)
  • Date: Fri, 13 Sep 2013 21:09:32 +0200
  • In-reply-to: <CAA1cxuj-OzXnGXt=ObdcoYyXVcz=G+s1v_g1YxNtyJYhrKiqOw@mail.gmail.com>
  • References: <CAA1cxuj-OzXnGXt=ObdcoYyXVcz=G+s1v_g1YxNtyJYhrKiqOw@mail.gmail.com>
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