ocaml - 可以用frama-c做头文件分析吗？

Question

我将 frama-c 视为在 OCaml 中处理 C 头文件的一种方式（例如，用于生成语言绑定）。它很有吸引力，因为它看起来是一个文档齐全且维护良好的项目。但是，经过大量谷歌搜索和文档搜索后，我找不到任何适合该目的的内容。我只是错过了执行此操作的正确方法，还是超出了 frama-c 的范围？与其他一些插件相比，这似乎是一件相当微不足道的事情。

Answer 1

正如 Pascal 所说，我认为从命令行是不可能的，但是因为无论如何您都必须编写一些代码，所以您可以设置 flag 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

开发插件将更适合更复杂的处理（请参阅开发人员手册），但脚本使其易于测试。

Answer 2

在当前状态下，不幸的是，不可能使用 Frama-C 来解析既未定义也未使用的函数声明。

日：

int mybinding (int x, int y);

这为您提供了标准化 AST 的视图。标准化意味着可以简化的所有内容是：

$ frama-c -print t.h
[kernel] preprocessing with "gcc -C -E -I.  t.h"
/* Generated by Frama-C */

不幸的是，由于mybinding既没有使用也没有定义，它被删除了。

可以选择保留带有规范的声明，但您想要的是保留所有声明的选项。我从来没有注意到这样的选择：

$ frama-c -kernel-help
...
-keep-unused-specified-functions  keep specified-but-unused functions (set by
                    default, opposite option is
                    -remove-unused-specified-functions)

保持功能符合规范的选项并不能满足您的要求：

$ frama-c -keep-unused-specified-functions -print t.h
[kernel] preprocessing with "gcc -C -E -I.  t.h"
/* Generated by Frama-C */