Получу ли я 3-х адресный код в Frama-c

Question

Я только начал разрабатывать плагин frama-c, который выполняет некоторый анализ псевдонимов. Я использую анализ Dataflow.Backwards, и теперь мне нужно пройти через различные операторы присваивания и собрать кое-что о lvalues.

Предоставляет ли frama-c 3-адресный код? Есть ли у меня какие-либо гарантии относительно формы lvalue (или какого-либо доступа к памяти)? Я имею в виду, что, как в саже или вале, что существует не более одного доступа к полю, st, для a->b->c, будет временная переменная, такая как tmp = a->b; tmp-> с;? Я проверил руководства, но не смог найти ничего, связанного с этим.

Answer 1

Следующий модуль из Cil, вероятно, делает то, что вам нужно: http://www.cs.berkeley.edu/~necula/cil/ext.html. Имейте в виду, что тип результирующего AST является стандартным Cil. Вы не получите никакой помощи от компилятора OCaml относительно того, какие конструкции могут присутствовать в упрощенном AST, а какие нет.

Также обратите внимание, что этот модуль до сих пор не был портирован на Frama-C. Вам понадобится небольшая адаптация, чтобы она работала в Frama-C.

Answer 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 ()