無限呼び出しチェックのレビューと修正

このトピックでは、Polyspace^® Code Prover™ で [無限呼び出し] チェックの結果を体系的にレビューする方法を説明します。

[無限呼び出し] チェックの修正を判断するまでこれらの手順の 1 つ以上に従います。このチェックを修正する方法は複数あります。チェックおよびコードの例については、無限呼び出しを参照してください。

チェックのレビューに関する一般的なワークフローについては、Polyspace デスクトップユーザーインターフェイスでの Code Prover の結果の解釈またはPolyspace Access Web インターフェイスでの Code Prover の結果の解釈 (Polyspace Access)を参照してください。

関数呼び出しに対する [無限呼び出し] レッドチェックは以下のいずれかを示します。

特定の呼び出しに失敗した関数本体内の操作。失敗が発生しない同じ関数への他の呼び出しがあるため、操作の失敗は通常、オレンジチェックとして関数本体内に表示されます。
他の理由で関数がその呼び出しコンテキストに返されない。たとえば、関数本体内のループが終了しない。

手順 1: チェックの根本原因の判定

関数本体内でチェックの根本原因を判定します。以下の手順は、Polyspace ユーザーインターフェイスでのみ実行できます。

関数定義に移動します。
レッドチェックを含む関数呼び出しを右クリックします。オプションが存在する場合、[定義に移動] を選択します。
関数本体内に終了条件を満たすことのないループがあるかどうかを判定します。
考えられる解決方法: 終了条件が満たされるようにコードまたは関数の引数を変更します。
それ以外の場合は、関数本体内で関数呼び出しに対して [無限呼び出し] レッドチェックの原因となったオレンジチェックを特定します。
見ただけではオレンジチェックが見つからない場合、解析オプション [状況依存性] を使用して検証を再実行します。オプションの引数として関数名を指定します。ソフトウェアは [無限呼び出し] レッドチェックの原因となるオレンジチェックをダークオレンジチェックとしてマークします。
詳細は、状況依存性 (-context-sensitivity)を参照してください。
オプションの使用に関するチュートリアルについては、ランタイムエラーのある関数呼び出しの特定を参照してください。
考えられる解決方法: オレンジチェックの原因を調べます。オレンジチェックを回避するためにコードまたは関数の引数を変更します。

手順 2: チェックの一般的な原因の検索

関数本体内のオレンジチェックに対して関数呼び出しの [無限呼び出し] をトレースするには、以下の手順を実行します。

関数呼び出しに引数が含まれる場合、関数本体内で関数パラメーターのすべてのインスタンスを検索します。パラメーターに関連するオレンジチェックを見つけることができるかを確認します。操作の失敗は同じ関数への他の呼び出しが原因ではないため、失敗はレッドの呼び出し内の関数パラメーター値に関連している可能性があります。
次の例では、func の本体内で arg1 と arg2 のすべてのインスタンスを検索します。変数名を右クリックして、[すべての参照を検索] を選択します。
```
void func(int arg1, double arg2) {
  . 
  .
}
 
void main() {
  int valInt1,valInt2;
  double valDouble1, valDouble2;
  . 
  .
  func(valInt1, valDouble1);
  func(valInt2, valDouble2);
}
```
func 内での操作の失敗は valInt1 と valDouble1 によって発生したものではないため、この失敗は valInt2 または valDouble2 が原因である可能性があります。valInt2 と valDouble2 は arg1 と arg2 にコピーされるため、オレンジチェックは arg1 または arg2 に関連する操作で発生しなければなりません。
関数呼び出しに引数が含まれていない場合、関数へのさまざまな呼び出しの間での差異を特定します。この差異の原因を関数本体内のオレンジチェックに関連付けられるかどうかを確認します。
たとえば、関数がグローバル変数を読み取る場合、関数への異なる呼び出しはグローバル変数の異なる値で操作される可能性があります。関数本体にグローバル変数に関連するオレンジチェックが含まれるかどうかを判定します。