Main Content

Non-terminating loop

Loop does not terminate or contains an error

Description

This check on a loop determines if the loop has one of the following issues:

  • The loop definitely does not terminate.

    The check appears only if Polyspace® cannot detect an exit path from the loop. For example, if the loop appears in a function and the loop termination condition is met for some function inputs, the check does not appear, even though the condition might not be met for some other inputs.

  • The loop contains a definite error in one its iterations.

    Even though a definite error occurs in one loop iteration, because the verification results in a loop body are aggregated over all loop iterations, the error shows as an orange check in the loop body. To indicate that a definite failure has occurred, a red Non-terminating loop check is shown on the loop command.

Unlike other checks, this check appears only when a definite error occurs. In your verification results, the check is always red. If the error occurs only in some cases, for instance, if the loop bound is variable and causes an issue only for some values, the check does not appear. Instead, the loop command is shown in dashed red with more information in the tooltip.

The check also does not appear if both conditions are true:

  • The loop has a trivial predicate such as for(;;) or while(1).

  • The loop has an empty body, or a body without an exit statement such as break, goto, return or an exception.

Instead, the loop statement is underlined with red dashes. If you place your cursor on the loop statement, you see that the verification considers the loop as intentional. If you deliberately introduce infinite loops, for instance, to emulate cyclic tasks, you do not have to justify red checks.

Using this check, you can identify the operation in the loop that causes the run-time error.

  • To find the source of error, on the Source pane, place your cursor on the function call and view the tooltip.

  • For loops with fewer iterations, you can navigate to the source of error in the loop body. Select the loop to see the full history of the result. Alternatively, right-click the loop keyword and select Go to Cause if the option exists.

Examples

expand all

#include<stdio.h>

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

In this example, in the while loop, i does not increase. Therefore, the test i<10 never fails.

Correction — Ensure Loop Termination

One possible correction is to update i such that the test i<10 fails after some loop iterations and the loop terminates.

#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;
  }
}

In this example, the last run of the for loop contains an Out of bounds array index error. Therefore, the Non-terminating loop check on the for loop is red. A tooltip appears on the for loop stating the maximum number of iterations including the one containing the run-time error.

Correction — Avoid loop iteration containing error

One possible correction is to reduce the number of loop iterations so that the Out of bounds array index error does not occur.

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);
}

In this example, the call to function assignValue in the last for loop iteration contains an error. Therefore, although an error does not show in the for loop body, a red Non-terminating loop appears on the loop itself.

Correction — Avoid loop iteration containing error

One possible correction is to reduce the number of loop iterations so the error in the call to assignValue does not occur.

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++;
  }
}

In this example, an Overflow error occurs in iteration number 31. Therefore, the Non-terminating loop check on the while loop is red. A tooltip appears on the while loop stating the maximum number of iterations including the one containing the run-time error.

Correction — Reduce loop iterations

One possible correction is to reduce the number of loop iterations so that the overflow does not occur.

#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();
}

In this example, the variable toUpdate might have the value 0 or a nonzero value depending on the call context of foo().

  • If the value is 0, the loop is not entered.

  • If the value is nonzero, the loop is entered but within the loop, the variable toUpdate is never updated.

Combining these two situations, the loop when entered does not terminate. Code Prover shows a red Non-terminating loop check on the while keyword.

In this example, the definition of the function runUpdates is not available to the analysis. Therefore, the analysis stubs the function and assumes that the function does not update global variables, including the variable toUpdate. For more information on how to work around assumptions on stubbed functions, see Code Prover Assumptions About Stubbed Functions.

Check Information

Group: Control flow
Language: C | C++
Acronym: NTL