ocaml - Frama-c はヘッダー ファイルの解析に使用できますか?

Question

OCamlでCヘッダーファイルを処理する方法としてframa-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

より複雑な処理にはプラグインの開発が適していますが (それについては開発者マニュアルを参照してください)、スクリプトを使用すると簡単にテストできます。

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 */