Frama-CコードスライサーがCファイルをロードしていません

Question

教授が書いた10個の数学アルゴリズムを持つ1000行のCファイルがあります。1000個の行から9個の数学関数とすべての依存関係を削除する必要があります。 Frama-C Boron windowsバイナリインストーラを使用してください。

ここでは、最も単純なexample.cファイルはロードされません...私はソースファイルを選択し、何もロードしません。

ボロン版は2010年のものですので、後でFrama-Cをコンパイルする方法を確認しました。私のWindows 7のユーザー名にスペースがあると言うと、問題が発生する可能性があります。

Frama-Cは私のスライス作業に最適ですか？ここで

はなりません負荷ファイルの例です：

// File swap.c: 

    /*@ requires \valid(a) && \valid(b); 
     @ ensures A: *a == \old(*b) ; 
     @ ensures B: *b == \old(*a) ; 
     @ assigns *a,*b ; 
     @*/ 
    void swap(int *a,int *b) 
    { 
     int tmp = *a ; 
     *a = *b ; 
     *b = tmp ; 
     return ; 
    } 

ここで私は滑らかでswvdラベルオプションから一つだけの機能を取ることを希望するコードです。 https://sites.google.com/site/kootsoop/Home/cohens_class_code

Answer 1

あなたがリンクしたコードを見ましたが、それはFrama-C解析のための最良の候補のようではありません。例えば、そのコードは厳密にはC99に準拠していない。いくつかの古いスタイルのプロトタイプ（暗黙的なintの戻り値の型を含む）、前方宣言なしで定義される関数（fft）、およびヘッダーのインクルード（stdlib.h）がありません。変更は比較的単純で、その一部はgcc -std=c99の動作と同様に扱われるため、大きな問題ではありません。警告は出すがエラーは出ません。ただし、ゼロ以外の時間が必要であることに注意することが重要です。したがって、これはプラグアンドプレイのソリューションではありません。

より一般的な注意点として、Frama-CはCコードの正規化にCIL (C Intermediate Language)を依存しているため、スライスされたプログラムは「元のプログラムからスライスされた文を除いたもの」とはおそらく同じではありません。目的が単にいくつかのステートメントを削除するだけで、コードを構文上はまったく同じに保つのであれば、Frama-Cは理想的ではありません。

最後に、デッドコードを見つけるのに役立つFrama-C解析がいくつかあり、コードがすでに関数に分割されていると結果がさらに明確になることは注目に値する。たとえば、適切に構成されたプログラムでバリュー分析を使用すると、実行されないステートメントや関数を確認することができます。しかし、これは少なくともいくつかの未定義の振る舞いがないことに依存しています。

など。初期化されていない変数がプログラムで使用されている場合（C標準では禁止されていますが、時折発生し、気付かない場合）、バリュー分析はその伝播を停止し、その後コードはという意味で dead w.r.t標準。素朴なアプローチは誤解を招くので、それを認識することが重要です。

全体として、あなたが言及しているコードサイズでは、特にFrama-Cを使用したことがなく、コンパイルに問題がある場合、Frama-Cは費用対効果の高い方法ではないでしょうか？ （2）あなたのコードベースをすでに知っていて、その部分を手動でスライスすることに比較的熟練しているならば、

私はそのようなステートメントを保存するCスライサーは知らないと言いました。直感的には、Cスライサーが構文の大部分を単純に保持すると考えるかもしれないが、Cはそれほど難しい言葉ではないので、ほとんどのツールがいくつかの正規化ステップをあらかじめ行っているのはなぜか。