0

私は frama-c Aluminium-20160502 バージョンを使用しており、大規模なプログラムの依存関係を調べたいと考えています。コマンド ラインでオプション -deps を使用すると、いくつかの依存関係が欠落していることがわかりました。特に、複数の条件が 1 つの if に結合されている場合、依存関係の分析は、1 つの条件が false になるたびに停止します。この例では、次のとおりです。

#include<stdio.h>
#include<stdbool.h>

/*Global variable definitions*/
bool A = true;
bool B = false;
bool C = true;
bool X;
bool Y;

bool res;


void main(){

        if (A && B && C) {
                res = X;
        }else res = Y;
}

私が試したとき：frama-c -deps program.c

フレームは、次の依存関係を示しています。

[from] ====== 計算された依存関係 ======

これらの依存関係は、終了する実行の終了時に保持されます。

[from] 関数 main: res FROM A; B; よ

[from] ====== 依存関係の終わり ======

したがって、条件 B は既に false であるため、条件 C には到達しません。

条件が満たされていない場合でも、すべての依存関係を計算するように frama に指示する方法があるのだろうか。オプション -slevel を試してみましたが、結果はありませんでした。間隔 Frama_C_interval(0,1) を使用する方法があることは知っていますが、それを使用すると、この関数を使用する変数が依存関係に表示されません。X と Y を A、B、C に依存させ、res を A、B、C、X、Y に依存させたい

何か案は？

4

1 に答える 1

0

From プラグインは、値分析プラグインの結果を使用します。あなたの例では、 と の値Aは十分に正確であるため、 ValueBは に到達する前に条件が完全に決定されていると推測できます (&&演算子は左から右に遅延評価されるため) C。Cフロムの視点から。

残念ながら、Frama_C_intervalグローバル初期化子で直接使用することはできません:

user error: Call to Frama_C_interval in constant.

ただし、「ハック」を使用できます (常に最適な解決策ではありませんが、ここでは機能します)。

volatile bool nondet;
bool A = nondet;
bool B = nondet;
bool C = nondet;
...

nondetであるためvolatile、各変数A、Bおよび にCは異なる非決定論的値が割り当てられることに注意してください。

この場合、 Value は条件の両方の分岐を考慮する必要があるため、実行中に読み取られるC可能性があるため、例では依存関係になります。次に、次のようになります。Cmain

       These dependencies hold at termination for the executions that terminate:
[from] Function main:
  res FROM A; B; C; X; Y

一部のプラグインでは、揮発性変数を処理する際に特別な処理が必要になるため、これが常に最適なソリューションであるとは限りません。

ただし、これは一部の種類の依存関係のみを扱います。Value Analysis ユーザー マニュアルの第 6 章で説明されているように、From プラグインは、機能的、命令的、および運用上の依存関係を計算します。これらには、言及したように、 などの間接的な制御依存関係は含まれません。そのためには PDG (Program Dependence Graph) プラグインが必要ですが、現時点では依存関係のテキスト出力はありません。を使用して計算し、依存関係グラフをドット (graphviz) 形式でエクスポートできます。これがあなたの関数から得られるものです（前述の揮発性ハックを使用）：X from A, B, C-pdg-pdg-dot <file>main

メイン関数の PDG

最後に、補足として:-slevelは主に精度を向上させるために使用されますが、あなたの例ではすでに精度が高すぎます(つまり、 Value はC内部で読み取られることはないと推測できますmain)。

于 2016-11-18T12:51:10.387 に答える