メインコンテンツ

このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。

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

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

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

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. [無限ループ] のレッドの結果を選択します。[ソース] ペインで mainfor ループが強調表示されます。

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

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

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

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

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

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

メモ

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

参考

トピック