Review and Fix Non-Terminating Loop Checks
This topic describes how to systematically review the results of a Non-terminating loop check in Polyspace® Code Prover™.
Follow one or more of these steps until you determine a fix for the Non-terminating
loop check. There are multiple ways to fix the check. For a description
of the check and code examples, see Non-terminating loop
.
For the general workflow on reviewing checks, see Interpret Code Prover Results in Polyspace Desktop User Interface or Interpret Code Prover Results in Polyspace Access Web Interface (Polyspace Access).
Step 1: Interpret Check Information
Place your cursor on the loop keyword such as for
or while
.
Obtain the following information from the tooltip:
Whether the loop is infinite or contains a run-time error.
In the following example, it is likely that the loop is infinite.
If the loop contains a run-time error, the number of loop iterations. Because Polyspace considers that execution stops when a run-time error occurs, from this number, you can determine which loop iteration contains the error.
In the following example, it is likely that the loop contains a run-time error. The error is likely to occur on the 31st loop iteration.
Step 2: Determine Root Cause of Check
If the loop is infinite, determine why the loop-termination condition is never satisfied.
If you deliberately have an infinite loop in your code, such as for cyclic applications, you can add a comment and justification in your result or code. See Address Results in Polyspace User Interface Through Bug Fixes or Justifications or Address Results in Polyspace Access Through Bug Fixes or Justifications (Polyspace Access).
If the loop contains a run-time error, identify the error that causes the Non-terminating loop check. Fix the error.
In the loop body, the run-time error typically occurs as an orange check of another type on an operation. The check is orange and not red because the operation typically passes the check in the first few loop iterations and fails only in a later iteration. However, because the failure occurs every time the loop runs, the Non-terminating loop check on the loop keyword is red.
For loops with few iterations, you can navigate directly from the loop keyword to the operation causing the run-time error.
To find the source of error, on the Source pane, select the red loop keyword. The Result Details pane shows the full history leading to the operation that causes the run-time error.
Navigate to the source of error in the loop body. Right-click the loop keyword and select Go to Cause if the option exists.
For a tutorial, see Identify Loop Operation with Run-Time Error.
Step 3: Look for Common Causes of Check
If the loop is infinite:
Check your loop-termination condition.
Inside the loop body, see if you change at least one of the variables involved in the loop-termination condition.
For instance, if the loop-termination condition is
while (count1 + count2 < count3)
, see if you are changing at least one ofcount1
,count2
, orcount3
in the loop.If you are changing the variables involved in the loop-termination condition, see if you are changing them in the right direction.
For instance, if the loop termination condition is
while(i<10)
and you decrementi
in the loop, the loop does not terminate. You must incrementi
.
If the loop contains a run-time error:
If the loop control variable is an array index, see if you have an orange Out of bounds array index error in the loop body.
If the loop control variable is passed to a function, see if you can relate the red Non-terminating loop error to an orange error in the function body.