我刚刚开始开发一个 frama-c 插件,该插件正在执行某种别名分析。我正在使用 Dataflow.Backwards 分析,现在我必须遍历不同的赋值语句并收集一些有关左值的内容。
frama-c 是否为我提供 3 地址代码?我对左值(或任何内存访问)的形状有一些保证吗?我的意思是,就像在 soot 或 wala 中那样,最多有一个字段访问,s.t.,对于 a->b->c,会有一个像 tmp=a->b 这样的临时变量; tmp->c;?我检查了手册,但找不到与此相关的任何内容。
最佳答案
不,Frama-C 中没有这种标准化。如果您确实需要它,您可以首先使用访问者来标准化代码,使其适合您的插件的要求。事情会是这样的:
class normalize prj: Visitor.frama_c_visitor =
object
inherit Visitor.frama_c_copy prj
method vinstr i =
match i with
| Set (lv,e) -> ...
....
end
let analyze () = ...
let run () =
let my_prj = File.create_project_from_visitor "my_project" (fun prj -> new normalize prj) in
Project.on my_prj analyze ()
关于frama-c - 我可以在 Frama-c 中获得 3 地址代码吗,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/15557464/