Frama-C:获取语句的值 [英] Frama-C: Getting the values of statement

问题描述

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

I want to develop a Frama-C-Plugin, where I get the values of the current statement.

借助此帖子 Frama-C插件开发:获得价值分析的结果我能够打印语句的值，但是指针并未以我需要的方式显示.

With the help of this post Frama-C Plugin development: Getting result of value-analysis I was able to print the values of the statements, but Pointers were not shown the way I need it.

借助注释，我能够打印整个状态(不仅是语句的变量).

With the help of the comments, I was able to print the whole state (not only the variables of the statement).

我可以结合这两个:获取语句的变量，但也可以使用取消引用的指针(值)吗?

Can I combine these two: Get the variables of the statement, but also with pointers dereferenced (the value)?

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

For example, printing a non-pointer after statement x=1 results in x -> {{ NULL -> {1} }}, while printing a pointer, after a statement like *x=3, results in x -> {{ y -> {0} }} because the 0 is the offset of the variable, but I want to get the value where the pointer points to, in the example 3. The way I want it, would be to get something like that: x -> 3.

更好的是获取(String varname, int value)的元组，以便我自己打印.

Even better would be to get a tuple of (String varname, int value), so I can print it myself.

推荐答案

变量的值取决于其类型.因此，如果变量的类型为int，则其值为整数，但如果变量的类型为int*，则其值为int变量的地址.变量可以具有许多其他类型，例如结构，数组等.

The value of a variable depend on its type. So if the variable has type int, its value is an integer, but if the variable has the type int*, its value is the address of an int variable. The variable may have many other types such as structure, array, etc.

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

From you example, it seems that you want to get the value of the variable pointed by the pointer. Notice that in some cases, this is not a valid operation...

无论如何，我想您可以从

Anyway, I suppose that you can extract this function to print a lvalue from the previous answer in 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

然后，您可以使用以下信息打印所需的信息:

You can then print the information you are looking for with:

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

这篇关于Frama-C:获取语句的值的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！