無限ループ

ループが終了しないかまたはループにエラーがある

説明

このループに対するチェックはループに次のいずれかの問題があるかどうかを判別します。

ループが明確に終了しない。
このチェックは Polyspace^® がループの出口パスを検出できない場合のみ表示されます。たとえば、ループが関数内にあり、一部の関数入力でループ終了条件が満たされる場合には、その他の入力では条件を満たしていなくてもチェックは表示されません。
ループの反復の 1 つに明確なエラーが 1 つある。
明確なエラーが 1 回のループ反復で発生していても、ループ本体の検証結果はすべてのループ反復に集約されているため、エラーはループ本体にオレンジチェックとして表示されます。明確な失敗が発生していることを示すために [無限呼び出し] のレッドチェックがループコマンドに表示されます。

他のチェックと異なり、このチェックは明確なエラーが発生する場合のみ表示されます。検証結果では、チェックは常にレッドとなります。エラーが特定の状況 (ループ境界が可変で、一部の値に対してのみ問題が発生するなど) でのみ発生する場合、このチェックは表示されません。代わりに、ループコマンドが赤い破線で詳細情報とともにツールヒントに表示されます。

以下の条件が両方 true の場合にも、チェックは表示されません。

for(;;) や while(1) など、ループにトリビアルな述部が含まれている。
ループ本体が空、またはループ本体に break、goto、return、例外などの終了ステートメントが含まれていない。

代わりに、ループステートメントに赤い破線の下線が付けられます。このループステートメントにカーソルを置くと、検証ではループが意図的と見なされていることがわかります。たとえば、周期タスクをエミュレートするために意図的に無限ループを導入している場合、レッドチェックを正当化する必要はありません。

このチェックを使用して、ランタイムエラーの原因となるループ内の操作を特定できます。

エラーのソースを見つけるには、[ソース] ペインで関数呼び出しにカーソルを置きツールヒントを見ます。
反復数の少ないループの場合、ループ本体のエラーのソースに移動できます。ループを選択して結果の完全な履歴を表示します。あるいは、ループキーワードを右クリックして、オプションがあれば [原因に移動] を選択します。

このチェックの診断

無限ループチェックのレビューと修正

例

すべて展開する

ループが終了しない

#include<stdio.h>

void main() {
  int i=0;
  while(i<10) {
    printf("%d",i);
  }
}

この例では、while ループにおいて i が増加しません。したがって、i<10 のテストが失敗することはありません。

修正 — ループの終了を確保

1 つの修正方法として、i を更新し、ループの何回かの反復後にテスト i<10 が失敗してループが終了するとします。

#include<stdio.h>

void main() {
  int i=0;
  while(i < 10) {
    printf("%d",i);
    i++;
  }
}

ループが範囲外の配列インデックスエラーを含む

void main() {
  int arr[20];
  for(int i=0; i<=20; i++) {
    arr[i]=0;
  }
}

この例では、for ループの最後の実行に [範囲外の配列インデックス] エラーが含まれています。したがって、for ループに対する [無限ループ] チェックはレッドになります。ツールヒントが for ループ上に表示され、反復の最大回数が、ランタイムエラーが生じた反復を含めて示されます。

修正 — エラーのあるループ反復を回避

1 つの修正方法として、ループ反復の回数を減らし、[範囲外の配列インデックス] エラーが起きないようにします。

void main() {
  int arr[20];
  for(int i=0; i<20; i++) {
    arr[i]=0;
  }
}

ループに関数呼び出しエラーがある

int arr[4];

void assignValue(int index) {
  arr[index] = 0;
}

void main() {
  for(int i=0;i<=4;i++)
    assignValue(i);
}

この例では、最後の for ループ反復で、関数 assignValue の呼び出しにエラーが発生します。したがって、for ループ本体にはエラーが示されませんが、[無限ループ] のレッドエラーがループそのものに表示されます。

修正 — エラーのあるループ反復を回避

1 つの修正方法として、ループ反復の回数を減らし、assignValue の呼び出しでエラーが発生しないようにします。

int arr[4];

void assignValue(int index) {
  arr[index] = 0;
}

void main() {
 for(int i=0;i<4;i++)
   assignValue(i);
}

ループにオーバーフローエラーが含まれる

#define MAX 1024
void main() {
 int i=0,val=1;
 while(i<MAX) {
   val*=2;
   i++;
  }
}

この例では、[オーバーフロー] エラーが 31 番目の反復で発生します。したがって、while ループに対する [無限ループ] チェックはレッドになります。ツールヒントが while ループ上に表示され、反復の最大回数が、ランタイムエラーが生じた反復を含めて示されます。

修正 — ループ反復数を削減

1 つの修正方法として、ループ反復の回数を減らし、オーバーフローが起きないようにします。

#define MAX 30
void main() {
 int i=0,val=1;
 while(i<MAX) {
   val*=2;
   i++;
  }
}

ループに入るとループが終了しない

#include <stdbool.h>

bool toUpdate;
void runUpdates(void);

void foo() {
    while(toUpdate) 
       runUpdates();
}

この例では、foo() の呼び出しコンテキストに応じて、変数 toUpdate に値 0 あるいは非ゼロの値が格納されます。

値が 0 の場合、ループには入りません。
値が非ゼロの場合はループに入りますが、ループ内で変数 toUpdate が更新されることはありません。

これら 2 つの状況が組み合わされ、このループは無限ループになります。Code Prover は、while キーワードにレッドの [無限ループ] チェックを表示します。

この例での関数 runUpdates の定義は、解析で使用できません。したがって、解析ではこの関数をスタブし、この関数によって変数 toUpdate を含むグローバル変数が更新されることはないと仮定します。スタブ関数に関する仮定を回避する方法の詳細については、スタブ関数に関する Code Prover の仮定を参照してください。

チェック情報

グループ: 制御フロー

言語: C | C++

頭字語: NTL

参考

無限呼び出し