3

Frama-C プラグインの開発方法を学んでいます。Frama-C 開発者マニュアルを読み、CFG プラグインの例を実行した後、すべての注釈を C ファイルに出力する基本的なスクリプトを実行しようとしました。私はこれを思いついた：

open Cil_types

class print_annot out = object
    inherit Visitor.frama_c_inplace

method vstmt_aux s =
let annots = Annotations.code_annot s in
let anleng = List.length annots in
if anleng <= 0 then Format.fprintf out "Empty List\n"
  else
  Format.fprintf out "Number of Annotations: %d\n" anleng;
  List.iter (fun annot -> Format.fprintf out " -> s%d\n" annot.annot_id) annots;
  Cil.DoChildren
end

let run () =
let chan = open_out "annots.out" in
let fmt = Format.formatter_of_out_channel chan in
Visitor.visitFramacFileSameGlobals (new print_annot fmt) (Ast.get());
close_out chan

let () = Db.Main.extend run

入力ファイルにACSL注釈があり、注釈IDが出力されない場合でも、常にリストが空であると表示されます。私は何を間違っていますか？

編集：

次のコードの例:

 /*@ requires y >= 0;
 @ ensures \result >= 0;
 */

 int g(int y){
int x=0;

if(y>0){
    x=100;
    x=x+50;
    x=x-100;
}else{
    x = x - 150;
    x=x-100;
    x=x+100;
}
return x;
    }

    void main(){
int a = g(0);

 }

そして、frama-c を次のように呼び出します。

 $ frama-c -load-script annot_script.ml condi.c

次の出力が得られます。

 Empty List
 Empty List
 Empty List
 Empty List
 Empty List
 Empty List
 Empty List
 Empty List
 Empty List
 Empty List
 Empty List
4

1 に答える 1

3

あなたの例では、注釈はステートメントに添付されていません。requiresとensuresは関数コントラクトの一部であり、 のステートメントではなく、関数に関連付けられていgますg。

ステートメントに添付される注釈は、たとえば/*@ assert x == 150; */行の後にありますx=x+50;。

condi.cこのアサーションを挿入するように変更すると、同じコマンドラインで次のようになります。

空のリスト
空のリスト
空のリスト
空のリスト
注釈の数: 1
 -> s1
空のリスト
空のリスト
空のリスト
空のリスト
空のリスト
空のリスト
空のリスト

ステートメントに添付された注釈の印刷に対応する「期待」の値に対して、スクリプトは期待どおりに機能しているようです。

于 2014-05-07T19:39:12.707 に答える