Review and Fix Overflow Checks

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

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

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 operation that overflows.

Cursor placed over an operation that overflows with the tooltip showing for the check.

Obtain the following information from the tooltip:

The operand variable you can constrain to avoid the overflow.
In the preceding example, the left operand, val, has full range of values.
Possible fix: To avoid the overflow, perform the multiplication only if val is in a certain range.
```
if(val < INT_MAX/2)
    return(val*2);
else 
    /* Alternate action */
```
The probable root cause for overflow, if indicated in the tooltip.
In the preceding example, the software identifies a stubbed function, getVal, as probable cause.
Possible fix: To avoid the overflow, constrain the return value of getVal. For instance, specify that getVal returns values in a certain range, for example, 1..10. For more information, see Code Prover Assumptions About Stubbed Functions.

Step 2: Determine Root Cause of Check

Trace the data flow starting from the operand variable that you want to constrain. Identify a suitable point to specify your constraint.

In the following example, trace the data flow starting from tempVal.

val = func();
.
.
tempVal = val;
.
.
tempVal++ ;

In this example, you might find that:

tempVal obtains a full-range of values from val.
Possible fix: Assign val to tempVal only if val is less than a certain value.
val obtains a full-range of values from func.
Possible fix: Constrain the return value of func, either in the body of func or through the Polyspace Constraint Specification interface, if func is stubbed. For more information, see Code Prover Assumptions About Stubbed Functions.

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 the previous write operation on the operand variable.
  Example: The previous write operation on tempVal is tempVal=val.
2. At the previous write operation, identify a new variable to trace back.
  Place your cursor on the variables involved in the write operation to see their values. The values help you decide which variable to trace.
  Example: At tempVal=val, you find that val has a full-range of values. Therefore, you trace val.
3. Find the previous write operation on the new variable. Continue tracing back in this way until you identify a point to specify your constraint.
  Example: The previous write operation on val is val=func(). You can choose to specify your constraint on the return value of func.

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.

Tip

To distinguish between integer and float overflows, use the Detail column on the Results List pane. Click the column header so that integer and float overflows are grouped together. If you do not see the Detail column, right-click any other column header and enable this column.

Step 3: Look for Common Causes of Check

If the operation causing the overflow occurs in a loop or in the body of a recursive function:

See if you can reduce the number of loop runs or recursions.
See if you can place an exit condition in the loop or recursive function before the operation overflows.

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 are using a volatile variable in your code. Then:

Polyspace assumes that the volatile variable is full-range at every step in the code.
An operation using that variable can overflow and is therefore orange.
If you know that the variable takes a smaller range of values, add a comment and justification in your code 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.