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 将 return 计算 k 的表达式，而 deref_vi vi_n 将 return 对应于 ***vi_n。你应该调整你的函数来做或多或少相同的事情，尤其是在 TPtr

的情况下

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

Frama-C-Plugin: Resolve Pointer to pointer

frama-c