このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。
PolyspaceCode Prover のオレンジ チェック
Polyspace® Code Prover™ は、特定のランタイム エラーに対して C/C++ コードの各操作をチェックし、結果をレッド、グリーンまたはオレンジ チェックとして表示します。詳細は、Code Prover の結果とソース コードの色を参照してください。このトピックでは、Polyspace Code Prover 解析の結果のオレンジ チェックについて説明します。
オレンジ チェックが発生した場合
オレンジ チェックは、Polyspace が潜在的なランタイム エラーを検出したが、証明できないことを表します。ある操作のチェックは、両方の条件が true である場合にオレンジで表示されます。
| 第 1 の条件 | 第 2 の条件 | 例 |
|---|---|---|
| この操作が、1 つの実行パスまたは複数の実行パス上に複数回現れる場合。 | 静的検証中に、操作が失敗する回数や失敗するパスはごくわずかである場合。 | 操作が発生する場合。
|
| 複数の値を取る変数が操作に含まれる場合。 | 静的検証中に、操作が失敗する値はごくわずかである。 | 操作が volatile 変数を含む。 |
静的検証中は、Polyspace は実行中に現れる実行パスよりも多くの実行パスを考慮することが可能です。操作がパスのサブセット上で失敗した場合、Polyspace はそのサブセットが実行中に実際に出現したかどうかを判定できません。したがって、レッド チェックの代わりに、操作に対して オレンジ チェックが生成されます。
複数のパスによるオレンジ チェック
以下の例を考えてみます。
void main() {
func(1);
func(0);
}
double func(int value) {
return (1.0/value); //Orange check
}func は 2 つの引数で 2 回呼び出されます。1 回の呼び出しのみでは、func の本体内でゼロ除算が発生します。Code Prover では、この結果が [ゼロ除算] オレンジ チェックとして表示されます。
不明な値によるオレンジ チェック
以下の例を考えてみます。
double func(int value) {
int reducedValue = value%21 - 10; // Result in [-10,10]
return 1.0/reducedValue; //Orange check
}func の呼び出しコンテキストが不明な場合、Code Prover では、その引数 value が任意の int 値を取る可能性があると仮定されます。その結果、reducedValue は [-10,10] の任意の値を取る可能性があります。これらのいずれかの値がゼロの場合、func 内でゼロ除算が発生します。Code Prover では、この結果が [ゼロ除算] オレンジ チェックとして表示されます。
次の理由により、値が不明になり、以降は広範にわたって Code Prover の仮定が行われる場合があります。
定義のない関数:定義されていない関数によって、値が不明になる可能性があります。
解析時に関数定義を利用できない場合、Code Prover 解析で関数がスタブ化されます。解析では、スタブ関数の戻り値と、そのスタブ関数が呼び出される場所での他の二次的影響について特定の仮定が行われます。スタブ関数に関する Code Prover の仮定も参照してください。
呼び出しコンテキストのない関数:解析するコード内の他の場所では呼び出されない関数によって、値が不明になる可能性があります。
解析するプログラムに
main関数が含まれていない場合は、Code Prover がmainを生成します。既定では、生成されたmainは、そのデータ型で許容される任意の値を取ることができる引数を使用しなければ呼び出されない関数を呼び出します。参考:グローバル変数:
main関数がない場合、グローバル変数によって、値が不明になる可能性があります。解析するプログラムに
main関数が含まれていない場合は、Code Prover がmainを生成します。既定では、生成されたmainは呼び出した各関数の開始時に、グローバル変数がそのデータ型で許容される任意の値を取ることができると仮定します。グローバル変数の初期化に関する Code Prover の仮定も参照してください。
通常は、ファイルごとに解析すると、表示されるオレンジ チェックの数が多くなります。これは、(インクルードされたヘッダーとともに) 1 つのファイルからなる個別の解析ユニットごとに main 関数が含まれる可能性は低いためです。したがってこのモードでは、main がない場合の解析に必要となる、あらゆる仮定がトリガーされます。ファイルごとの解析についての詳細は、ファイルを個別に検証 (-unit-by-unit) を参照してください。
オレンジ チェックをレビューする理由
Polyspace では情報が失われることはないため、実際の実行パスのスーパーセットを考慮するのは適切な近似です。操作がランタイム エラーを含む場合、Polyspace は操作にグリーン チェックを生成しません。Polyspace が、近似のためにランタイム エラーを証明できない場合、オレンジ チェックが生成されます。したがって、オレンジ チェックはレビューする必要があります。
Polyspace 近似は例として以下を含みます:
実行パスの特定ポイントにおける、変数範囲の近似。たとえば、Polyspace は
[-1,10]により変数floatの範囲{-1} U [0,10]を近似できます。マルチタスキング コードでの、命令のインターリーブの近似。たとえば、一組みのタスクにおいて特定の命令が相互に割り込みしない場合でも、Polyspace 検証はこれを考慮しない場合があります。
オレンジ チェックをレビューする方法
実行中に操作が失敗しないことを確実にするには、以下を行います。
操作が失敗する実行パスが実際に発生するかどうかを判定する。
詳細は、次を参照してください。
いずれかの実行パスが発生する可能性があれば、失敗の原因を修正します。
実行パスが発生しない場合、Polyspace の結果もしくはソース コードにコメントを入力し、そのパスが発生しない理由を記述します。詳細は、以下を参照してください。
後の検証では、結果にこれらのコメントをインポートできます。このとき、後の検証でオレンジ チェックが残っている場合にも、再度レビューを行う必要はありません。
オレンジ チェックを減らす方法
Polyspace が近似を実行する理由は以下のいずれかです。
コードがランタイム実行に関する完全な情報を含んでいない。たとえば、コードが部分的に開発されているか、値が既知なのは実行時のみである変数を含んでいる。
オレンジ チェックを減らす場合、Polyspace に必要な情報を提供します。詳細は、検証用のコンテキストを提供するを参照してください。
コードが極めて複雑である。たとえば、複数の型変換や複数の
gotoステートメントが存在する。オレンジ チェックを減らす場合、コードの複雑さを減らし、推奨のコーディング方法に従います。詳細は、Polyspace Bug Finder を使用してコーディング ルールに従うを参照してください。
Polyspace は適切な時間内に検証を完了させ、適切なコンピューター リソースを使用しなければならない。
オレンジ チェックを減らす場合、検証の精度を向上させます。しかし、精度を高めると検証時間も増加します。詳細は、検証精度の向上を参照してください。
