frama-c - 我可以在 Frama-c 中获得 3 地址代码吗

Question

我刚刚开始开发一个 frama-c 插件，该插件正在执行某种别名分析。我正在使用 Dataflow.Backwards 分析，现在我必须遍历不同的赋值语句并收集一些有关左值的内容。

frama-c 是否为我提供 3 地址代码？我对左值(或任何内存访问)的形状有一些保证吗？我的意思是，就像在 soot 或 wala 中那样，最多有一个字段访问，s.t.，对于 a->b->c，会有一个像 tmp=a->b 这样的临时变量； tmp->c;？我检查了手册，但找不到与此相关的任何内容。

Answer 1

不，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 ()