-improve-pointer-analysis-precision

Enable more precise pointer analysis mode in Code Prover

Since R2022a

Syntax

-improve-pointer-analysis-precision

Description

This option is not required since R2023b. The precise analysis mode enabled by this option is available by default.

-improve-pointer-analysis-precision enables a more precise pointer analysis mode in Code Prover. In this mode, the analysis can keep a more precise record of the relationship between pointers and pointed variables, and can show more precise results for run-time checks if the execution paths leading to the checks involve pointers.

If you are running an analysis from the user interface (Polyspace^® desktop products only), on the Configuration pane, you can enter this option in the Other field. See Other.

Examples

Improved Analysis Precision on Structures Cast to Another Type

In this example, a pointer to a structure is cast to a pointer to char and then its contents are initialized. Because of the cast, the later fields of the original structure stay non-initialized. Without this option, the analysis cannot prove the non-initialized state of the later fields and shows an orange check when those fields are read. If you use this option, because of the improved pointer analysis, you can see a red check.

struct myStruct {
  int firstField;
  int secondField;
};
int foo(){
  struct myStruct obj;
  struct myStruct *ptr = &obj;
  *(char *)ptr = 1;
  return obj.secondField; 
}

To see the improved pointer analysis, use the option with the polyspace-code-prover or polyspace-code-prover-server command:

Code Prover:

polyspace-code-prover -sources filename -improve-pointer-analysis-precision

Code Prover Server:

polyspace-code-prover-server -sources filename -improve-pointer-analysis-precision

Improved Analysis Precision on Higher Dimensional Arrays

In this example, a two-dimensional array of type std::array is initialized in a for loop. Without this option, the analysis cannot prove the fully initialized state of the array and shows an orange check when the first array element is read post-initialization. If you use this option, because of the improved pointer analysis, you can see a green check.

#include <array>

float func() {
    const size_t sz = 10;
    std::array <std::array<float, sz>, sz> twoDArray;
    
    for(int row = 0; row < sz; row++) {
        for (int col = 0; col < sz; col++) {
            twoDArray[row][col] = 0;
        }
    }
    
    float initValue = twoDArray[0][0];
    return initValue;
}

To see the improved pointer analysis, use the option with the polyspace-code-prover or polyspace-code-prover-server command:

Code Prover:

polyspace-code-prover -sources filename -improve-pointer-analysis-precision

Code Prover Server:

polyspace-code-prover-server -sources filename -improve-pointer-analysis-precision

Tips

This option keeps a more precise record of the relations between pointers and pointed variables and might not scale to large applications.
The new pointer analysis does not support multitasking. If you use one of the multitasking options, the analysis falls back to the previous mode.
You can constrain external pointers to point to arrays such that only the first element of the array is initialized to values in a certain range. For pointers constrained this way, if you use the option -increase-pointer-analysis-precision, the analysis correctly considers only the first array element as initialized. Without the option, all elements of the array are considered as initialized (though the constrained range is applied only to the first element).
For instance, in the following example, if you constrain the pointer p this way, reading the second element p[1] leads to a red Non-initialized variable check:
```
int* p;
void main() {
   int x = p[0];
   int y = p[1]; //Red check here
}
```
You can impose this constraint by selecting SINGLE for the option Init Allocated in your constraint specifications. See also External Constraints for Polyspace Analysis.

Version History

Introduced in R2022a