2013-02-06 4 views
6

私はframam-cをOCamlのCヘッダファイルを処理する方法(例えば、言語バインディングを生成するため)として探していました。それは非常によく文書化され、維持されているプロジェクトのように思えるので魅力的です。しかし、多くのグーグルとドキュメントの検索の後、私は目的に適したものを見つけることができません。私はちょうどこれを行うための正しい方法がないか、それともframa-cの範囲外ですか?それは他のプラグインのいくつかと比較して、それが行うことはかなり些細なもののように思えます。ヘッダーファイル解析にframa-cを使用できますか?

+0

これは正確にはわからないが、CIL(http://kerneis.github.com/cil/)の助けを借りればよいだろうと思う。 –

+0

ポインタのおかげで - cilのドキュメントを突き抜け、有用なものがあれば参照してください –

答えて

5

、私はそれが可能であるとは思わない、私はそのようなオプションに気づいたことがありませんとにかくコードを書く必要があるため、フラグ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: %[email protected]]@ @[%s at %[email protected]]@]@]@." 
     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 

プラグインを開発するより適切であろうより複雑な処理が必要な場合は(Developer Manualを参照してください)、スクリプトをテストするのは簡単です。

+0

ありがとう!私はframa - cをあきらめなければならないのではないかと恐れていた –

1

現状では、残念ながらFrama-Cを使用して、定義されていない関数や宣言されていない関数の宣言を解析することはできません。

t.h:

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 */ 
関連する問題