無限ループ チェックのレビューと修正
このトピックでは、Polyspace® Code Prover™ で [無限ループ] チェックの結果を体系的にレビューする方法を説明します。
[無限ループ] チェックの修正を判断するまでこれらの手順の 1 つ以上に従います。このチェックを修正する方法は複数あります。チェックおよびコードの例については、無限ループを参照してください。
チェックのレビューに関する一般的なワークフローについては、Interpret Polyspace Code Prover Results in Polyspace Platform User InterfaceまたはPolyspace Access Web インターフェイスでの Code Prover の結果の解釈 (Polyspace Access)を参照してください。
チェック情報の解釈
for または while などのループ キーワードにカーソルを置きます。
ツールヒントから次の情報を取得します。
ループが無限である、あるいはランタイム エラーを含んでいるかどうか。
次の例では、ループは無限である可能性があります。
ループにランタイム エラーが含まれている場合のループの反復回数。Polyspace はランタイム エラー発生時に実行が停止すると見なすため、この数値からどのループ反復にエラーが含まれているのかを特定できます。
次の例では、ループにランタイム エラーが含まれている可能性があります。エラーは 21 回目のループ反復で発生する可能性があります。
チェックの根本原因の判定
ループが無限である場合、ループ終了条件が満たされることがない理由を特定します。
コード内の無限ループが周期的なアプリ用など意図的なものである場合、結果またはコードにコメントおよび正当化情報を追加できます。バグ修正または正当化による Polyspace の結果への対処またはPolyspace Access でのバグ修正または正当化による結果への対処 (Polyspace Access)を参照してください。
ループにランタイム エラーが含まれている場合、[無限ループ] チェックの原因となるエラーを特定します。エラーを修正します。
ループ本体内では通常、ランタイム エラーは操作に対して別のタイプのオレンジ チェックとして発生します。このチェックはオレンジであり、レッドではありません。操作が通常、最初の数回のループ反復でチェックをパスし、後の反復でのみ失敗するためです。ただし、失敗はループが実行されるたびに発生するため、ループ キーワードの [無限ループ] チェックはレッドです。
反復が数回のループでは、ランタイム エラーを起こしている操作にループ キーワードから直接移動できます。
エラーのソースを見つけるには、[ソース] ペインで赤いループ キーワードを選択します。[結果の詳細] ペインで、ランタイム エラーを起こしている操作につながる完全な履歴が表示されます。
ループ本体でエラーのソースまで移動します。ループ キーワードを右クリックして、オプションがあれば [原因に移動] を選択します。
チュートリアルについては、ランタイム エラーのあるループ操作の特定を参照してください。
チェックの一般的な原因の検索
ループが無限の場合、次の手順に従います。
ループ終了条件をチェックします。
ループ本体内部で、ループ終了条件に含まれる変数の少なくとも 1 つを変更するかどうかを確認します。
たとえば、ループ終了条件が
while (count1 + count2 < count3)である場合、ループ内のcount1、count2またはcount3の少なくとも 1 つを変更しているかどうかを確認します。ループ終了条件に含まれる変数を変更している場合、正しい方向に変数を変更しているかどうかを確認します。
たとえば、ループ終了条件が
while(i<10)でiをデクリメントする場合、ループは終了しません。iをインクリメントしなければなりません。
ループにランタイム エラーが含まれる場合、次の手順に従います。
ループ制御変数が配列インデックスである場合、ループ本体内に [範囲外の配列インデックス] オレンジ エラーがあるかどうかを確認します。
ループ制御変数が関数に渡される場合、関数本体内でレッドの [無限ループ] エラーをオレンジ エラーに関連付けられるかどうかを確認します。
