Как можно сопоставить код CLI frama- c с исходным оператором c? И как мне найти документацию по API-интерфейсу frama- c? - PullRequest
Новая
       29

Как можно сопоставить код CLI frama- c с исходным оператором c? И как мне найти документацию по API-интерфейсу frama- c?

0 голосов
/ 05 марта 2020

Я пытаюсь получить график зависимости программы (PDG), используя frama- c на уровне оператора исходного кода. Однако подключаемый модуль 'pdg' в frama- c печатает PDG на уровне узла анализируемого кода.

Поскольку frama- c - gui может выделить исходный оператор, соответствующий узлу в анализируемый код, я почти уверен, что существует соответствие между узлом в разобранном коде и оператором исходного кода. Как я могу получить это отображение? Просто номер строки в исходном коде тоже подойдет.

1 Ответ

2 голосов
/ 06 марта 2020

Frama- C * GUI представляет два вида кода:

  1. Код CIL (C Промежуточный язык), часто называемый нормализованный исходный код , что соответствует красивой печати AST Frama, в верхней центральной панели;
  2. и оригинальный исходный код, в верхней правой панели.

Я предполагаю что по проанализированному коду вы говорите о CIL (нормализованном) коде .

Каждый элемент в AST Frama- C содержит местоположение , которая является парой позиций : первая и последняя координаты (строка, строка, столбец) в исходном коде, которые соответствуют этому элементу (минус несколько исключений, такие как сгенерированные элементы, расширения макросов и т. д. c). У большинства элементов AST есть способы получить это местоположение.

В случае узлов PDG вы можете получить соответствующие операторы (если есть) и затем распечатать их местоположение, как показано в коде ниже (запустите с frama-c -pdg -load-module print_pdg.ml <file> ): 

(* print_pdg.ml *)
let () = Db.Main.extend (fun () ->
    Globals.Functions.iter (fun kf ->
        let pdg = !Db.Pdg.get kf in
        !Db.Pdg.iter_nodes (fun n ->
            match PdgTypes.Node.stmt n with
            | None -> ()
            | Some st ->
              Format.printf "%a: %a@."
                Printer.pp_location (Cil_datatype.Stmt.loc st) Printer.pp_stmt st
          ) pdg
      )
  )

Обратите внимание, что мой пример сценария будет печатать каждый оператор несколько раз, если с одним оператором связано несколько узлов PDG.

По умолчанию Printer.pp_location печатает только имя файла и строка начального символа, но вы можете создать собственный симпатичный принтер для включения столбца или координат последнего символа.

API и документация по подключаемым модулям (из вопроса в комментарии )

Некоторые плагины Frama- C (Eva, WP, E-ACSL и др. c.) Имеют свои собственные руководства, которые доступны для загрузки в Frama- C page .

Специфического руководства c для плагина Pdg не существует, но некоторые сгенерированные Ocamldo c страницы HTML можно получить из Frama- C API архив .

Однако, что Большинство разработчиков плагинов Frama- C предпочитают использовать плагин OCaml Merlin в своем любимом редакторе (emacs, vim, et c) для навигации по коду и чтения комментариев источника. (например, в файлах .mli).

Например, в Emacs C-c C-l для имени модуля / переменной переходит к его определению, а C-c C-a чередуется между .ml и .mli файлы (реализация - документация). В сочетании с автозаполнением для обнаружения модулей / функций это обеспечивает форму интерактивной документации, которая удобна для многих разработчиков OCaml.

...