Review and Fix Out of Bounds Array Index Checks

This topic describes how to systematically review the results of an Out of bounds array index check in Polyspace^® Code Prover™.

Follow one or more of these steps until you determine a fix for the Out of bounds array index check. There are multiple ways to fix the check. For a description of the check and code examples, see Out of bounds array index.

Sometimes, especially for an orange check, you can determine that the check does not represent a real error but a Polyspace assumption that is not true for your code. If you can use an analysis option to relax the assumption, rerun the verification using that option. Otherwise, you can add a comment and justification in your result or code.

For the general workflow that applies to all 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 [ symbol.

Obtain the following information from the tooltip:

Array size. The allowed range for array index is 0 to (array size - 1).
Actual range for array index

In the preceding example, the array size is 10. Therefore, the allowed range for the array index is 0 to 9. However, the actual range is 0 to 10.

Possible fix: To avoid the out of bounds array index, access the array only if the index is between 0 and (array size - 1).

#define SIZE 100
int arr[SIZE];
.
.
if(i<SIZE)
	val = arr[i]
else
	/*Error handling */

Step 2: Determine Root Cause of Check

If you want to know or change the array size, right-click the array variable and select Go To Definition, if the option exists. Otherwise, trace the data flow starting from the array index variable. Identify a point where you can constrain the index variable.

To trace the data flow, select the check, and note the information on the Result Details pane.

If the Result Details pane shows the sequence of instructions that lead to the check, select each instruction.
If the Result Details pane shows the line number of probable cause for the check, right-click the Source pane. Select Go To Line.
Otherwise:
1. Find previous instances of the array index variable.
2. Browse through those instances. Find the instance where you constrain the array index variable to (array size - 1).
  Possible fix: If you do not find an instance where you constrain the index variable, specify a constraint for the variable. For example:
```
if(index<SIZE)
	read(array[index]);
```
3. Determine if the constraint applies to the instance where the Out of bounds array index error occurs.
  For example, you can constrain the index variable in a for loop using for(index=0; index<SIZE; index++). However, you access the array outside the loop where the constraint does not apply.
  Possible fix: Investigate why the constraint does not apply. See if you have to constrain the index variable again.
4. If the index variable is obtained from another variable, trace the data flow for the second variable. Determine if you have constrained that second variable to (array size - 1).

Depending on the variable, use the following navigation shortcuts to find previous instances. You can perform the following steps in the Polyspace user interface only.

Variable How to Find Previous Instances of Variable

Variable	How to Find Previous Instances of Variable
Local Variable	Use one of the following methods: Search for the variable. Right-click the variable. Select Search For All References. All instances of the variable appear on the Search pane with the current instance highlighted. On the Search pane, select the previous instances. Browse the source code. Double-click the variable on the Source pane. All instances of the variable are highlighted. Scroll up to find the previous instances.
Global Variable Right-click the variable. If the option Show In Variable Access View appears, the variable is a global variable.	Select the option Show In Variable Access View. On the Variable Access pane, the current instance of the variable is shown. On this pane, select the previous instances of the variable. Write operations on the variable are indicated with and read operations with .
Function return value ret=func();	Find the function definition. Right-click `func` on the Source pane. Select Go To Definition, if the option exists. If the definition is not available to Polyspace, selecting the option takes you to the function declaration. In the definition of `func`, identify each `return` statement. The variable that the function returns is your new variable to trace back.

Local Variable

Use one of the following methods:

Search for the variable.
1. Right-click the variable. Select Search For All References.
  All instances of the variable appear on the Search pane with the current instance highlighted.
2. On the Search pane, select the previous instances.
Browse the source code.
1. Double-click the variable on the Source pane.
  All instances of the variable are highlighted.
2. Scroll up to find the previous instances.

Global Variable

Right-click the variable. If the option Show In Variable Access View appears, the variable is a global variable.

Select the option Show In Variable Access View.
On the Variable Access pane, the current instance of the variable is shown.
On this pane, select the previous instances of the variable.
Write operations on the variable are indicated with and read operations with .

Function return value

ret=func();

Find the function definition.
Right-click func on the Source pane. Select Go To Definition, if the option exists. If the definition is not available to Polyspace, selecting the option takes you to the function declaration.
In the definition of func, identify each return statement. The variable that the function returns is your new variable to trace back.

You can also determine if variables in any operation are related from some previous operation. See Find Relations Between Variables in Code.

Step 3: Look for Common Causes of Check

Look for common causes of the Out of bounds array index check.

See if you are starting the array index variable from 0.
In the condition that constrains your array index variable, see if you use <= when you intended to use <.
If a check occurs in or immediately after a for or while loop, determine if you have to reduce the number of runs of the loop.
If you use the sizeof function to constrain your array, see if you are dividing sizeof(array) by sizeof(array[0]) to obtain the array size.
sizeof(array) returns the array size in bytes.

Step 4: Trace Check to Polyspace Assumption

See if you can trace the orange check to a Polyspace assumption that occurs earlier in the code. If the assumption does not hold true in your case, add a comment or 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).

For instance, you constrain the array index using a function whose definition you do not provide. Then:

Polyspace cannot determine that the array index variable is constrained.
When you use this variable as array index, an Out of bounds array index error can occur.
If you know that the variable is constrained to the array size, add a comment and justification describing why you did not change your code.

For more information, see Code Prover Analysis Assumptions.

Note

Before justifying an orange check, consider carefully whether you can improve your coding design.

For instance, constraining a global variable in one function and using it as array index in a second function causes vulnerabilities in your code. If a new function is called between the previous two functions and modifies your global variable, the constraint no longer applies.