2

実際にスレッド化された C コードを評価するために、frama-c 値アナライザーを試しています。発生する可能性のあるスレッドの問題を無視して、単一のスレッドの可能な値を調べるだけです。これまでのところ、エントリ ポイントをスレッドの開始位置に設定することで機能します。

ここで私の問題: あるスレッド内で、別のスレッドによって書き込まれた値を読み取ります。これは、frama-c がスレッド化を考慮していない (またすべきではない) (現在のところ)、変数が広い範囲にあると想定しているためです。範囲は実際にははるかに小さいです。値アナライザーにこの変数の値の範囲を伝えることは可能ですか?

例：

volatile int x = 0;

void f() {
    while(x==0)
        sleep(100);
    ...
}

ここで、frama-c は x が揮発性であり、したがって [--..--] の範囲を持っていることを検出しますが、他のスレッドが x に何を書き込むかを知っているので、アナライザーに x が 0 または 1 しかできないことを伝えたいと考えています。特にGUIで、これはframa-cで可能ですか？

前もってありがとうクリスチャン

4

2 に答える 2

3

これは現在、自動的にはできません。値の分析では、volatile 変数には、基になる型に含まれる値の全範囲が常に含まれていると見なされます。ただし、揮発性変数へのアクセスをユーザー指定の関数の呼び出しに変換する独自のプラグインが存在します。あなたの場合、コードは本質的に次のように変換されます。

int x = 0;

void f() {
while(1) {
    x = f_volatile_x();
    if (x == 0)
    sleep(100);
...
}

正しく指定するf_volatile_xことで、0 から 1 の間の値のみを返すようにすることができます。

于 2012-06-13T13:17:51.653 に答える
2

調査中のスレッドで変数「x」が変更されていない場合は、「main」関数の先頭で次のように初期化することもできます。

x = Frama_C_interval (0, 1);

これは Frama-C で定義された関数である...../share/frama-c/builtin.cため、使用するときはこのファイルを入力に追加する必要があります。

于 2012-06-15T10:23:31.567 に答える