Review and Fix Correctness Condition Checks

This topic describes how to systematically review the results of a Correctness condition check in Polyspace^® Code Prover™.

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

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

On the Results List pane, select the check. View the cause of check on the Result Details pane. The following list shows some of the possible causes:

An array is converted to another array of larger size.
In the following example, a red check occurs because an array is converted to another array of larger size.
When dereferenced, a function pointer has value NULL.
In the following example, a red check occurs because, when dereferenced, a function pointer has value NULL.
When dereferenced, a function pointer does not point to a function.
In the following example, an orange check occurs because Polyspace cannot determine if a function pointer points to a function when dereferenced. This situation can occur if, for instance, you assign an absolute address to the function pointer.
A function pointer points to a function, but the argument types of the pointer and the function do not match. For example:
```
typedef int (*typeFuncPtr) (complex*);
int func(int* x);
.
.
typeFuncPtr funcPtr = &func;
```
In the following example, a red check occurs because:
- The function pointer points to a function func.
- func expects an argument of type int, but the corresponding argument of the function pointer is a structure.
A function pointer points to a function, but the argument numbers of the pointer and the function do not match. For example:
```
typedef int (*typeFuncPtr) (int, int);
int func(int);
.
.
typeFuncPtr funcPtr = &func;.
```
In the following example, a red check occurs because:
- The function pointer points to a function func.
- func expects one argument but the function pointer has two arguments.
A function pointer points to a function, but the return types of the pointer and the function do not match. For example:
```
typedef double (*typeFuncPtr) (int);
int func(int);
.
.
typeFuncPtr funcPtr = &func;
```
In the following example, a red check occurs because:
- The function pointer points to a function func.
- func returns an int value, but the return type of the function pointer is double.
The value of a variable falls outside the range that you specify through the Global Assert mode. See Constrain Global Variable Range for Polyspace Analysis.
In the following example, a red check occurs because:
- You specify a range 0...10 for the variable glob.
- The value of the variable falls outside this range.

Step 2: Determine Root Cause of Check

Based on the check information on the Result Details pane, perform further steps to determine the root cause. You can perform the following steps in the Polyspace user interface only.

Check Information How to Determine Root Cause

Check Information	How to Determine Root Cause
An array is converted to another array of larger size.	To determine the array sizes, see the definition of each array variable. Right-click the variable and select Go To Definition. If you dynamically allocate memory to an array, it is possible that their sizes are not available during definition. Browse through all instances of the array variable to find where you allocate memory to the array. 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.
Issues when dereferencing a function pointer: The function pointer has value `NULL` when dereferenced. The function pointer does not point to a function when dereferenced. The function pointer points to a function, but the argument types of the pointer and the function do not match. The function pointer points to a function, but the argument numbers of the pointer and the function do not match. The function pointer points to a function, but the return types of the pointer and the function do not match.	Find the location where you assign the function pointer to a function. Right-click the function pointer. Select Search For All References. All instances of the function pointer appear on the Search pane with the current instance highlighted. On the Search pane, select the previous instances. Determine the argument and return types of the function pointer type and the function. Identify if there is a mismatch between the two. For instance, in the following example, determine the argument and return types of `typeFuncPtr` and `func`. typeFuncPtr funcPtr = func; Right-click the function pointer type and select Go To Definition. Right-click the function and select Go To Definition. If the definition does not exist, this option shows the function stub definition instead. In this case, find the function declaration. Sometimes, you assign a function pointer to a function with matching signature, but the assignment is unreachable. Check if this is the case.
The value of a variable falls outside the range that you specify through the Global Assert mode.	Browse through all previous instances of the global variable. Identify a suitable point to constrain the variable. Right-click the variable. Select Show In Variable Access View. On the Variable Access pane, select each instance of the variable.

An array is converted to another array of larger size.

To determine the array sizes, see the definition of each array variable.
Right-click the variable and select Go To Definition.
If you dynamically allocate memory to an array, it is possible that their sizes are not available during definition. Browse through all instances of the array variable to find where you allocate memory to the array.
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.

Issues when dereferencing a function pointer:

The function pointer has value NULL when dereferenced.
The function pointer does not point to a function when dereferenced.
The function pointer points to a function, but the argument types of the pointer and the function do not match.
The function pointer points to a function, but the argument numbers of the pointer and the function do not match.
The function pointer points to a function, but the return types of the pointer and the function do not match.

Find the location where you assign the function pointer to a function.
1. Right-click the function pointer. Select Search For All References.
  All instances of the function pointer appear on the Search pane with the current instance highlighted.
2. On the Search pane, select the previous instances.
Determine the argument and return types of the function pointer type and the function. Identify if there is a mismatch between the two. For instance, in the following example, determine the argument and return types of typeFuncPtr and func.
```
typeFuncPtr funcPtr = func;
```
1. Right-click the function pointer type and select Go To Definition.
2. Right-click the function and select Go To Definition. If the definition does not exist, this option shows the function stub definition instead. In this case, find the function declaration.
Sometimes, you assign a function pointer to a function with matching signature, but the assignment is unreachable. Check if this is the case.

The value of a variable falls outside the range that you specify through the Global Assert mode.

Browse through all previous instances of the global variable. Identify a suitable point to constrain the variable.

Right-click the variable. Select Show In Variable Access View.
On the Variable Access pane, select each instance of the variable.

Step 3: 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).