可以使用frama-c进行头文件分析吗？

Question

我在将frama-c看作是在OCaml中处理C头文件的一种方法(例如,用于生成语言绑定).它很有吸引力,因为它看起来像是一个记录良好且维护良好的项目.然而,经过大量的谷歌搜索和搜索文档后,我找不到任何适合此目的的东西.我只是错过了正确的方法,或者它是否超出了frama-c的范围？与其他一些插件相比,它似乎是一件相当简单的事情.

Answer 1

正如Pascal所说,我不认为从命令行可以,但是因为你必须编写一些代码,你可以设置标志Rmtmps.keepUnused.这是一个可用于查看声明的脚本:

let main () =
  Rmtmps.keepUnused := true;
  let file = File.from_filename "t.h" in
  let () = File.init_from_c_files [ file ] in
  let _ast = Ast.get () in
  let show_function f =
    let name = Kernel_function.get_name f in
    if not (Cil.Builtin_functions.mem name) then
      Format.printf "Function @[<2>%a:@ @[@[type: %a@]@ @[%s at %a@]@]@]@."
        Kernel_function.pretty f
        Cil_datatype.Typ.pretty (Kernel_function.get_type f)
        (if Kernel_function.is_definition f then "defined" else "declared")
        Cil.d_loc (Kernel_function.get_location f)
in Globals.Functions.iter show_function

let () = Db.Main.extend main

要运行它,您必须使用如下-load-script选项:

$ frama-c -load-script script.ml

开发插件更适合于更复杂的处理(参见" 开发人员手册 "),但脚本可以轻松进行测试.