Frama-C：获取语句的值

Question

我想开发一个 Frama-C-Plugin，我可以在其中获取当前语句的值。

在这个 post 的帮助下，我能够打印语句的值，但是指针没有按照我需要的方式显示。

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

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

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

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

Answer 1

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

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

无论如何，我想您可以提取此函数以打印中先前答案的左值：

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

Frama-C：获取语句的值

Frama-C: Getting the values of statement

ocaml

frama-c