Frama-c から後方スライスを取得しましたが、動的スライスではなく静的スライスのように見えます。
動的後方スライスを取得するためのframa-cの特定のオプションはありますか?
質問する
263 次
1 に答える
0
ウィキペディアによると、
動的スライスには、プログラムの任意の実行のプログラム ポイントで変数の値に影響を与えた可能性のあるすべてのステートメントではなく、プログラムの特定の実行のプログラム ポイントで変数の値に実際に影響を与えるすべてのステートメントが含まれます。
Frama-C のスライシング プラグインは、価値分析プラグインからの値によって調整されます。これは、関心のある一連の実行で実行に発生するすべての値を表すと信じています。Frama-C のスライシング プラグインを動的スライシング用に構成するには、値分析を 1 回の実行に対応させる必要があります。main入力なし、volatile変数なし、不明な関数の呼び出しなしの関数を使用し、オプション-slevel 999999999を渡すと、別の質問に対するこの以前の回答にframa-c記載されているように、選択したプログラムの単一の実行に沿って値分析が C インタープリターとして動作するはずです。このブログ投稿とこの記事で。
于 2014-10-24T21:47:33.230 に答える