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: abiao.yang at (David Yang)
  • Date: Fri, 13 Sep 2013 17:16:07 +0800

Dear all,

First of all, my question is: How to obtain a Base.t variable's original

A Base(the Base module in frama-c api) variable can be like this:
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:

I can iterate each variables by using :  Locations.Zone.map_i : (Base.t ->
Lattice_Interval_Set.Int_Intervals.t -> t) -> t -> t


For debugging, I output each base.t :

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: <>