Frama-C:获取语句值
Frama-C:获取语句值
提问于 2016-03-29 06:10:29
我想开发一个，在这里我得到当前语句的值。
在这篇文章Frama-C Plugin development: Getting result of value-analysis的帮助下，我能够打印语句的值，但是指针没有显示我需要它的方式。
在注释的帮助下，我能够打印整个状态(不仅仅是语句的变量)。
我可以组合这两个变量:获取语句的变量，但也可以使用取消引用的指针(值)吗？
例如，在语句x=1之后打印一个非指针将导致x -> {{ NULL -> {1} }}，而在*x=3这样的语句之后，打印指针将导致x -> {{ y -> {0} }}，因为0是变量的偏移量，但是我想要得到指针指向的值，在示例3中，我想要的方式是得到类似于x -> 3的内容。
更好的方法是获得一个(String varname, int value)的元组，这样我就可以自己打印了。
回答 1
Stack Overflow用户
回答已采纳
发布于 2016-03-29 09:14:30
变量的值取决于其类型。因此，如果变量具有int类型，则其值为整数，但如果变量具有int*类型，则其值为int变量的地址。该变量可能有许多其他类型，如结构、数组等。
从您的示例来看，您似乎希望得到指针所指向的变量的值。注意在某些情况下，这不是一个有效的操作.
无论如何，我认为您可以从Frama-C Plugin development: Getting result of value-analysis中的前一个答案中提取这个函数来打印一个lvalue。
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页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/36276698
复制相关文章
相似问题
腾讯云开发者
