Frama-C：ステートメントの値を取得する

Question

私は現在のステートメントの値を取得するFrama-C-Pluginを開発したいと思います。

Frama-C Plugin development: Getting result of value-analysis私はステートメントの値を印刷することができましたが、必要な方法でポインタが表示されませんでした。

コメントの助けを借りて、私は状態全体（文の変数だけでなく）を印刷することができました。

私はこれらの2つを組み合わせることができます：ステートメントの変数を取得するだけでなく、逆参照されたポインタ（値）も取得できますか？

ポインタを印刷中に0が変数のオフセットが、私がしたいされているため、例えば、x -> {{ NULL -> {1} }}に文の後x=1結果を非ポインタを印刷し、* X = 3のようなステートメントの後、x -> {{ y -> {0} }}になり例3のポインタが指している値を取得します。 私がそれを望む方法は、そのようなものを得ることです：x -> 3。

タプルを(String varname, int value)にすると、印刷することができます。

Answer 1

変数の値は、その型によって異なります。変数の型がintの場合、その値は整数ですが、変数の型がint*の場合、その値はintの変数のアドレスになります。変数には、構造体、配列などの他の多くの型がある可能性があります。

例から、変数 の値をポインタで指しているとします。いくつかのケースで、これは有効な操作ではないことに注意してください...とにかく

、私はあなたがFrama-C Plugin development: Getting result of value-analysisで前の回答から左辺値を印刷するには、この機能を抽出することができているとします

let pretty_lval fmt stmt lval = 
    let kinstr = Kstmt stmt in (* make a kinstr from a stmt *) 
    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_lval lval 
     Locations.Location_Bytes.pretty value (* print mapping *) 
    )() ~after:false kinstr 

あなたが、その後することができます探している情報を印刷してください：

if Cil.isPointerType vi.vtype then 
    let lval = (Mem (Cil.evar vi), NoOffset) in 
    pretty_lval fmt stmt lval