Frama-C-Plugin：将指针解析为指针

Question

我正在开发一个 frama-c-plugin，我想在其中获取指针的值（不是它们指向的地址，而是该地址的值）。

到目前为止，这适用于简单的指针。现在我想处理指向指针的指针。

例如：

int k=12;
int *l=&k;
int **m = &l;
int ***n = &m;

当用我的实际版本分析这段代码时，我得到了值：

k=12
l=12
m=&k
n=&l

但我想要这些值：

k=12
l=12
m=12
n=12

因为它们都使用值 12 引用相同的内存位置（通过多个引用）

现在我的问题是：是否有可能得到 m 和 n 的底值？

编辑

对不起，我对问题的描述不好，我在 Frama-C-GUI 中通过单击错误的变量犯了一个错误，这使我的问题变得混乱。我删除了最初问题的这一部分。

我的代码如下所示：

let rec rec_struct_solver vtype packed_fi vi_name act_offset=
    match vtype with
        | TComp( compinfo, bitsSizeofTypCache, attributes) ->(
            if compinfo.cstruct then (
                (*Do stuff for structs *)
            )
        )
        | TNamed (typeinfo, attributes) ->(
            (*Do Stuff for named types*)
        )
        | TPtr (typ1, attribute) -> (
            let rec loc_match typ2=
                match typ2 with
                    | TPtr(typ3, attribute) ->(
                        loc_match typ3
                    )
                    | TComp(_,_,_) -> (
                        rec_struct_solver typ2 None vi_name act_offset
                    )
                    | _ ->(
                        self#print_var_values stmt (Mem (Cil.evar vi), NoOffset) vi_name
                    )
            in
                loc_match typ1
        | _ -> (*do something for others*)

所以如果指针指向另一个指针，它应该递归地执行函数 loc_match，直到找到一个结构或非指针变量。

外部函数被调用：rec_struct_solver vtype None vi.vname NoOffset 我认为错误在 (Mem(Cil.evar vi), NoOffset) 部分，因为它只解决了第一个指针步骤，但我不知道我应该使用什么作为参数来构建 lval。

我希望问题现在更清楚了。

Answer 1

下面的代码可用于获取一个 cil 表达式，该表达式尽可能地取消引用一个变量。 （直到结果不再是指针。）

open Cil_types

let dummy_loc = Cil_datatype.Location.unknown
let mk_exp_lval lv = Cil.new_exp ~loc:dummy_loc (Lval lv)

(* Build ( *^n )e until [e] has no longer a pointer type.
   invariant: typ == Cil.typeOf e *)
let rec deref typ e =
  match Cil.unrollType typ with
  | TPtr (typ_star_e, _) ->
    let star_e (* *e *) = mk_exp_lval (Cil.mkMem e NoOffset) in
    deref typ_star_e star_e
  | _ -> e

(* Build ( *^n vi *)
let deref_vi vi =
  deref vi.vtype (mk_exp_lval (Var vi, NoOffset))

使用您的示例，deref_vi vi_k 将返回一个计算 k 的表达式，而 deref_vi vi_n 将返回对应于 ***vi_n 的 Cil 表达式。你应该调整你的函数来做或多或少相同的事情，尤其是在TPtr的情况下