3

ある種のエイリアス分析を行うframa-cプラグインの開発を始めたところです。私は Dataflow.Backwards 分析を使用していますが、さまざまな割り当てステートメントを調べて、左辺値に関する情報を収集する必要があります。

frama-c は 3 アドレス コードを提供しますか? 左辺値 (またはメモリアクセス) の形状について保証はありますか? つまり、soot や wala のように、a->b->c の場合、最大で 1 つのフィールド アクセス 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 型であることに注意してください。簡略化された AST に存在できるコンストラクトとそうでないコンストラクトについて、OCaml コンパイラからは何の助けも得られません。

このモジュールはこれまで Frama-C に移植されていないことにも注意してください。Frama-C 内で機能させるには、多少の調整が必要です。

于 2013-03-22T20:41:05.027 に答える