ランタイム エラーのあるループ操作の特定

このチュートリアルでは、ループ内でランタイム エラーを強調表示する Polyspace® Code Prover™ の結果を解釈する方法を示します。

エラーがループ内で発生する場合、エラーは解析結果に [無限ループ] レッド チェックとして、ループ キーワード (for、while など) 上に表示されます。

for (i = 0; i <= 10; i++)
エラーを起こす操作はループ内でオレンジ チェックとして表示されます。ループ内でこのオレンジ チェックと他のオレンジ チェックを区別するには、ランタイム エラーの原因となっている操作に赤いループ キーワードから直接移動します。

このチュートリアルでは、関数がループ内で呼び出されます。関数本体には別のループがあり、このループにランタイム エラーを起こす操作が含まれています。最初のループからランタイム エラーを起こす操作までトレースします。

  1. このコードに対して検証を実行し、結果を開きます。

    int a[100];

int f (int i);

void main() {
  int i,x=0;
  for (i = 0; i <= 10; i++) {
    x += f(i);
  }
}

int f (int i) {
  int j, x;
  x = 0;
  for (j = 0; j <= 10; j++) {
    x += a[10 + (i * j)];
  }
  return x;
}

  2. [無限ループ] のレッドの結果を選択します。[ソース] ペインで main の for ループが強調表示されます。

  3. main の for ループからエラーを起こす操作までトレースします。その操作は x+= a[10 + (i*j)] です。i が 9 で j が 10 の場合に [範囲外の配列インデックス] エラーが発生します。エラーは [ 演算子にオレンジで表示されます。

    赤い for キーワードからオレンジの配列アクセス操作までトレースするには、以下を行います。

    • 操作に直接移動します。for キーワードを右クリックし、[原因に移動] を選択します。

    • for キーワードから配列アクセス操作までの完全な履歴を確認します。赤い for キーワードを選択します。[結果の詳細] ペインに履歴が表示されます。

      イベント履歴は順番に読み取ることができます。外側のループはエラーなしで 9 回実行されます。10 回目の反復 (i=9) で、ループは関数 f に入ります。f 内で、内側のループはエラーなく 10 回実行されます。11 回目の反復 (j=10) で、配列アクセスによってエラーが発生します。

    この情報を使用して、配列アクセス操作のランタイム エラーの修正方法を判断できます。

メモ

反復数が少数回しかないループでは、エラーの根本原因に直接移動できます。

参考

トピック