Review Polyspace Code Prover Analysis Results

Polyspace^® Code Prover™ checks C/C++ code exhaustively and proves the absence of certain types of run-time errors (static analysis or verification). Whatever means you use for running the analysis, afterwards, you open the results in the Polyspace user interface.

Example Files

To follow the steps in this tutorial, run Polyspace using the steps in Run Polyspace Code Prover on Desktop. Alternatively, in the Polyspace user interface, open example results using Help > Examples > Code_Prover_Example.psprj. If you have loaded the example results earlier and made some changes, to load a fresh copy, select Help > Examples > Restore Default Examples.

Interpret Results

Review each Polyspace result. Find the root cause of the issue.

Start from the list of results on the Results List pane.

If the Results List pane covers the entire window, select Window > Reset Layout > Results Review.
If you do not see a flat list of results, but instead see them grouped, from the list, select None.

Click the Family column header to sort the results based on how critical they are. Select the red Illegally dereferenced pointer check in the file example.c. A red check indicates that the error happens on all execution paths considered in the analysis.

See the source code on the Source pane and further information about the result on the Result Details pane.

For the Illegally dereferenced pointer result, the message on the Result Details pane indicates that the pointer p has an allowed buffer of 400 bytes. It points to a location that begins at 400 bytes from the beginning of the buffer and points to a data type of 4 bytes.

To investigate further and find the root cause of the issue, right-click the variable p on the Source pane and select Search For All References. Click each search result to navigate to the corresponding location on the source code. At each location, place your cursor on the variable p to see a tooltip that describes the variable value at that point in the code.

You see that the pointer variable p is initialized to a 100-element int array. The pointer traverses the array in a for loop with 100 iterations and points to the end of the array. On the line with the red Illegally dereferenced pointer check, this pointer is dereferenced, resulting in dereference of a memory location outside the array.

Additional Information

See:

Address Results Through Bug Fix or Comments

Once you understand the root cause of a Polyspace finding, you can fix your code. Otherwise, add comments to your Polyspace results to fix the code later or to justify the result. You can use the comments to keep track of your review progress.

Right-click the variable p on the Source pane. Select Open Editor. The code opens in a text editor. Fix the issue. For instance, you can make the pointer point to the beginning of the array after the for loop. Changes to the code are highlighted below.

...
int i, *p = array;

for (i = 0; i < 100; i++) {
    *p = 0;
     p++;
}

p = array;

if (get_bus_status() > 0)
...

If you rerun the analysis, you do not see the red Illegally dereferenced pointer check.

Alternatively, if you do not want to fix the defect immediately, assign a status To investigate to the result. Optionally, add comments with further explanation.

If you assign a status No action planned, the result does not appear in subsequent runs on the same project.

Additional Information

See:

Manage Results

When you open the results of a Code Prover analysis, you see a list of run-time checks, coding rule violations or other results. To organize your review, you can narrow down the list or group results by file or result type.

For instance, you can:

Review only red and critical orange checks.
Click the Family column header to sort checks by color. Alternatively, you can filter out results other than red and orange checks. To begin filtering, click the icon on the column header.
You can review only the path-related orange checks because they are likely to be more critical. To filter out other checks, use the filters on the Information column. Clear the All filter and then select the filter Origin: Path related issue.
Review only the new results since the last analysis.
On the Results List pane toolbar, click the New button.
Review results in certain files or functions.
On the Results List pane toolbar, from the list, select File.

Additional Information

See: