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(;;)
orwhile(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.
Diagnosing This Check
Examples
Check Information
Group: Control flow |
Language: C | C++ |
Acronym: NTL |