Frama-C：プラグインで注釈を追加

Question

私はFrama-C-pluginを書いています。このプラグインでは、関数に注釈を追加したいと考えています（たとえば、関数名= "test"の場合、パラメータ== 1と言うrequire句を追加します）。

Annotations.add_requiresという関数が見つかりましたが、パラメータの一部（Emitter.t、Identified_predicates）がわかりません。 string-parameterは、述語の関数名または独自の名前ですか？

この機能を使用するにはどうすればよいですか？ 例を見せてもらえますか？

Answer 1

エミッタはあなたのプラグインを識別し、修正するものと宣言しなければなりません。あなたのケースでは、あなたが仕様にプロパティを追加すると、あなたがそれを構築することができます。今すぐ

let emitter = Emitter.create "My plugin" [ Emitter.Funspec ] 
    ~correctness:[] ~tuning:[] 

、kernel_functionのためにこれは最初のパラメータはに等しいという前提を構築する方法の例です。 1つ：

let add_pre kf = match Kernel_function.get_formals kf with 
    | [] ->() 
    | c_var::_ -> 
    let l_var = Cil.cvar_to_lvar c_var in 
    let var_term = Logic_const.tvar l_var in 
    let cnst_term = Logic_const.tinteger 1 in 
    let eq_pred = Logic_const.prel (Cil_types.Req, var_term, cnst_term) in 
    let pred = Logic_const.new_predicate eq_pred in 
    let bname = Cil.default_behavior_name in 
    Annotations.add_requires emitter kf ~behavior:bname [pred]