Frama-C：获取语句的值

Question

我想开发一个 Frama-C-Plugin，用于获取当前语句的值。

在这篇文章 Frama-C Plugin development: Getting result of value-analysis 的帮助下，我能够打印语句的值，但指针没有按我需要的方式显示。

在 cmets 的帮助下，我能够打印整个状态（不仅仅是语句的变量）。

我可以将这两者结合起来：获取语句的变量，还可以使用取消引用的指针（值）？

例如，在语句x=1 之后打印非指针会导致x -> {{ NULL -> {1} }}，而在像 *x=3 这样的语句之后打印指针会导致x -> {{ y -> {0} }}，因为 0 是变量的偏移量，但我想获取指针指向的值，在示例 3 中。 我想要的方式是得到类似的东西：x -> 3。

最好是得到一个(String varname, int value) 的元组，这样我就可以自己打印了。

Answer 1

变量的值取决于它的类型。因此，如果变量的类型为int，则其值为整数，但如果变量的类型为int*，则其值为int 变量的地址。变量可能有很多其他类型，例如结构体、数组等。

从你的例子看来，你想获取变量的值 由指针指向。请注意，在某些情况下，这不是一个有效的操作...

无论如何，我想你可以从Frama-C Plugin development: Getting result of value-analysis 中的上一个答案中提取这个函数来打印一个左值：

let pretty_lval fmt stmt lval =
  let kinstr = Kstmt stmt in (* make a kinstr from a stmt *)
  let loc = (* make a location from a kinstr + an lval *)
    !Db.Value.lval_to_loc kinstr ~with_alarms:CilE.warn_none_mode lval
  in
  Db.Value.fold_state_callstack
    (fun state () ->
       (* for each state in the callstack *)
       let value = Db.Value.find state loc in (* obtain value for location *)
       Format.fprintf fmt "%a -> %a@." Printer.pp_lval lval
         Locations.Location_Bytes.pretty value (* print mapping *)
    ) () ~after:false kinstr

然后您可以打印您正在寻找的信息：

if Cil.isPointerType vi.vtype then
  let lval = (Mem (Cil.evar vi), NoOffset) in
  pretty_lval fmt stmt lval