Understanding Changes in Polyspace Results After Product Upgrade

This topic describes how to interpret changes in results after upgrading Polyspace^® Code Prover™. For product upgrade instructions, see Update Polyspace Products or Install Update or Upgrade to New Version of Polyspace Access (Polyspace Access).

If you upgrade to a newer release of Polyspace, you can see some changes in results for the same analysis. Each release introduces many improvements in analysis precision. These improvements can lead to the same analysis (same source files and options) showing a difference in results before and after the upgrade.

This topic describes the kinds of differences you might see, why they might be expected and how you can understand those differences. For information on how to compare two sets of results, see Migrate Polyspace Projects After Product Upgrade.

Changes in Polyspace Code Prover Results

For the same source code and analysis configuration, you might see a change in results because of improvements to the Polyspace Code Prover analysis engine. In Code Prover, a change in result means a change in color for the same run-time check. When comparing results, you can focus only on new red, gray and orange checks. As explained later, new green checks are typically the result of an increase in precision.

For major differences in results of a specific type, see if you can trace the difference to a documented change in behavior or assumptions.
Check the release notes of all releases between your prior release and the release you upgraded to. Look in the Verification results section in the Release Notes for Polyspace Code Prover for changes in behavior of specific checks or changes in Code Prover assumptions. Major changes in behavior or assumptions are typically documented in the release notes.
For differences in results that cannot be traced to a documented change, see if you can attribute the change in color to an increase in verification precision.
In addition to documented major changes, each new release also involves many minor improvements in the verification algorithms. These improvements typically lead to an increase in verification precision (or at least maintain the same precision as before).
Run-time checks in Polyspace Code Prover can return results in one of three colors:
- Red (proof of definite error)
- Green (proof of definite absence of error)
- Red (unproven, probable error)
In addition, a gray color is used for code that is unreachable and therefore not checked for other run-time errors. For more details, see Code Prover Result and Source Code Colors.
An increase in precision indicates changes in color in the direction shown in this figure:
In other words, one of these things might happen:
- Orange to green or red: An operation that shows an orange color might now be red or green. Code Prover has a more precise knowledge of variable ranges when analyzing that operation, so the presence or absence of an error can be proven.
  During verification, to check if an operation causes run-time errors, Code Prover uses previously computed possible values of the operands. Some of these values might be accumulated from the code (from initializations and subsequent write operations along various paths), but some of them are results of approximations and cannot happen in practice. An increase in precision leads to fewer approximations, so fewer values that come solely from approximations. As a result, it is possible to obtain proof in a greater number of cases.
  Consider this simple, illustrative example:
```
x = initValue;
y = x - 1;

// Call below increases its second arg if the first is positive
incr_y_if_x_positive(x,&y);

// Later operations involving x and y
interval = x - y ;
if (x > 0)
   interval = x;
num = range / interval;
```
  In this example, to prove that there is no division by zero, Code Prover has to keep track of the fact that interval = x - y can be zero only if x > 0 (and the fact that the case x > 0 is handled later). Because of approximations, Code Prover might not be able to keep track of relations between variables such as x and y across several lines of code leading to an orange division by zero check. An increase in precision means that Code Prover is able to track such kinds of relations on more complex operations, leading to a green division by zero check.
- Red, green or orange to gray: An operation that was previously checked and showed one of red, green or orange colors is now proven unreachable and appears in gray.
  As before, lower precision means considering more values from approximations. So, a conditional branch such as:
```
if (x >= 0)
```
  that is unreachable can be considered reachable because of a negative value of x coming from approximations. With the increase in precision, this value might no longer be considered making it possible to prove that the branch is unreachable. If the branch is proven unreachable, red, green and orange checks inside the branch disappear.
For an individual check, it is easier to understand this change in direction of colors. However, these changes of colors in individual statements do not translate directly to changes in overall number of results of a certain color and type. For instance, some orange division by zero checks might turn green, but some green checks might also turn gray, leading to an overall increase or decrease in green division by zero checks. Therefore, when comparing results, instead of focusing on changes in overall numbers of checks, compare a few individual checks that changed color. In most cases, you will see that the color change is an expected result of an increase in precision.
In rare cases, you can see a decrease of precision (changes of colors in the opposite direction compared to what is described in this section). Typically, changes in Polyspace algorithms are vetted against a representative database of code samples to make sure that they do not cause significant decrease in precision or increase in analysis time.

Changes in Polyspace Bug Finder Results

For the same source code and analysis configuration, you might see a change in results because of improvements to the Polyspace Bug Finder™ analysis engine. In Bug Finder, a change in results falls in one of these categories: a new result appears, an existing result no longer shows up, or the same result appears on a different location in the source code.

Suppose that you see a new result in the current release. The new result might appear because of updates to a specific checker or from general updates to the analysis algorithm that affects the result locations for several checkers. To find more details, check the release notes of all releases between your prior release and the release you upgraded to.

Look in the Analysis results section of the Release Notes for Polyspace Bug Finder for updates to a specific coding rule or defect checker:
- Updates to existing defect checkers appear in a specific entry Updated Bug Finder defect checkers.
- Updates to existing external coding standard checkers appear in a specific entry Changes to external coding standards checking.
Look in the Reviewing results section of the Release Notes for Polyspace Bug Finder for changes in location of checker results. For instance, if a result previously appeared in separate instances of a macro, it might now be rolled up to the macro definition.