3

我刚开始开发一个进行某种别名分析的 frama-c 插件。我正在使用 Dataflow.Backwards 分析，现在我必须通过不同的赋值语句并收集一些关于左值的东西。

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

4

2 回答 2

2

不，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 ()
于 2013-03-22T08:54:20.410 回答
1

Cil 的以下模块可能满足您的需求： http ://www.cs.berkeley.edu/~necula/cil/ext.html#toc26 。请注意，生成的 AST 的类型是标准 Cil 类型。您不会从 OCaml 编译器获得关于哪些结构可以存在于简化的 AST 中，哪些不能存在的任何帮助。

另请注意，到目前为止，此模块尚未移植到 Frama-C。您需要进行一些小的调整才能使其在 Frama-C 中工作。

于 2013-03-22T20:41:05.027 回答