Frama-Cプラグインの開発：価値分析の結果を得る

Question

私は、価値分析を使ってFrama-Cのためのプラグインを開発しています。 私は単に各ステートメントの後に変数（値）の状態を出力したい（私は解決策は簡単だと思いますが、わかりませんでした）。

訪問者のvstmt_auxメソッドでDb.Value.get_stmt_stateの現在の状態を取得しました。

どのように変数の値を取得できますか？

PS：私はこの記事を見つけたが、それは助けにはならなかった、本当の解決策は存在しない、と説明の助けを借りて、私はそれを行うことができませんでした： How to use functions in Value.Eval_expr, Value.Eval_op etc modules of Frama-c Value plugin

Answer 1

は、ここでの具体的な例です

open Cil_types 

(* Prints the value associated to variable [vi] before [stmt]. *) 
let pretty_vi fmt stmt vi = 
    let kinstr = Kstmt stmt in (* make a kinstr from a stmt *) 
    let lval = (Var vi, NoOffset) in (* make an lval from a varinfo *) 
    let loc = (* make a location from a kinstr + an lval *) 
    !Db.Value.lval_to_loc kinstr ~with_alarms:CilE.warn_none_mode lval 
    in 
    Db.Value.fold_state_callstack 
    (fun state() -> 
     (* for each state in the callstack *) 
     let value = Db.Value.find state loc in (* obtain value for location *) 
     Format.fprintf fmt "%a -> %a@." Printer.pp_varinfo vi 
     Locations.Location_Bytes.pretty value (* print mapping *) 
    )() ~after:false kinstr 

(* Prints the state at statement [stmt] for each local variable in [kf], 
    and for each global variable. *) 
let pretty_local_and_global_vars kf fmt stmt = 
    let locals = Kernel_function.get_locals kf in 
    List.iter (fun vi -> pretty_vi fmt stmt vi) locals; 
    Globals.Vars.iter (fun vi _ -> pretty_vi fmt stmt vi) 

(* Visits each statement in [kf] and prints the result of Value before the 
    statement. *) 
class stmt_val_visitor kf = 
    object (self) 
    inherit Visitor.frama_c_inplace 
    method! vstmt_aux stmt = 
     (match stmt.skind with 
     | Instr _ -> 
     Format.printf "state for all variables before stmt: %a@.%a@." 
      Printer.pp_stmt stmt (pretty_local_and_global_vars kf) stmt 
     | _ ->()); 
     Cil.DoChildren 
    end 

(* usage: frama-c file.c -load-script print_vals.ml *) 
let() = 
    Db.Main.extend (fun() -> 
     Format.printf "computing value...@."; 
     !Db.Value.compute(); 
     let fun_name = "main" in 
     Format.printf "visiting function: %s@." fun_name; 
     let kf_vis = new stmt_val_visitor in 
     let kf = Globals.Functions.find_by_name fun_name in 
     let fundec = Kernel_function.get_definition kf in 
     ignore (Visitor.visitFramacFunction (kf_vis kf) fundec); 
     Format.printf "done!@.") 

これは理想からかけ離れており、出力は次のようになります。印刷する方法を、それぞれローカルおよびグローバル変数のために、与えられた関数内の各ステートメントの前の値によって計算された結果は、（下から上への関数を読んで）単純にCvalue.Model.pretty stateを使用するよりも醜いですが、それはさらなる修正のための基礎として役立ちます。

このスクリプトはFrama-Cマグネシウムでテストされています。

単に~after:trueとfold_state_callstackに~after:falseパラメータを置き換え、文の後の状態を取得します。以前のバージョンのコードでは、事前状態の値をすでにバインドしていた関数が使用されていましたが、そのような関数はポスト状態にエクスポートされていませんでした。したがって、fold_state_callstackを使用する必要がありますコールスタックごとの状態）。