Как сохранить типы переменных в файл, используя Frama- C - PullRequest
Новая
       24

Как сохранить типы переменных в файл, используя Frama- C

2 голосов
/ 09 февраля 2020

Я пытаюсь напечатать типы переменных в программе C, используя Frama- C. Я обнаружил, что эта информация представлена ​​в GUI, как показано на рисунке ниже. Тем не менее, я не могу найти способ вывести эту информацию в файл. Не могли бы вы предложить мне способ выполнения этой задачи с Frama- c? enter image description here

1 Ответ

2 голосов
/ 10 февраля 2020

Прямых решений из командной строки нет. Тем не менее, это может быть очень легко сделано с помощью простого сценария, такого как (не проверено) 

let print_type () =
  Ast.compute();
  Globals.Vars.iter
   (fun v _ ->
     Format.printf "Variable %a: %a@."
     Cil_datatype.Varinfo.pretty v
     Cil_datatype.Typ.pretty v.vtype)

let () = Db.Main.extend print_type

, который можно запустить с помощью frama-c -load-script <my_script.ml> <other args including source files>

Дополнительная информация о сценариях Frama- C (включая обширное учебное пособие) доступно в руководстве разработчика .

...