2

私がframa-c分析を使用するとき、私のcプログラム。frama-cのインパクトプラグインにバグが残っているようです。これが私のプログラムです。

#include<stdio.h>
int global;
int main()
{
    global = 12;
    int result = 0;
    if(global > 1)
    {
         result += 100;
    }
    else
    {
        result += 200;
    }
    return 0;
}

変数「グローバル」の影響を受けるすべての統計を見つけたいと思います。明らかに、ステートメント「result +=100;」変数「global」に関連する「ifcondition」のスコープ内にあるため、ステートメント「result +=100;」ハイライトである必要があります。ただし、実行結果は正しくないようです。

4

1 に答える 1

3

特別なオプションを使用しておらず、Frama-CのGUIでステートメントの影響分析を開始していることを前提としていますglobal = 12。そうでない場合は、より詳細な手順を提供してください。

プログラムではif (global > 1)、ステートメントにデータ依存関係があるため、命令が選択されglobal = 12ます。ただし、ステートメントresult += 100はImpactプラグインによって選択されません。この場合、制御の依存関係がないため、これは意図された動作です。elseのブランチifが死んでいることに注意してください。したがって、条件は常に真であるため、の実行result += 100は実際にはの評価に依存しません。if (global > 1)制御フローは常にresult += 100命令に到達するため、制御依存関係は存在しません。

この例でコントロールの依存関係を示したい場合、最も簡単な方法は、行global = 12を次のように変更することです。

global = Frama_C_interval(0,100);

$(SHARE)/frama-C/libc/__fc_builtin.cそして、ファイルをコマンドラインに追加します。コントロールの依存関係のため、2つの命令result += 100と が選択されます。result += 200

于 2012-11-30T00:24:02.893 に答える