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 Platform user interface, open example results using Help > Prove absence of C runtime errors.

Interpret Results

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

Open your results in the Review perspective. When you first select your result file from the Results pane, the Project Overview dashboard opens. Select Review from the toolbar to open the Review perspective containing all results and details.

Start from the list of results on the Results List pane. If the Results List pane covers the entire window, select Layout > Reset.

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.

View code information on the Source Code 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.

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.

If you do not want to fix the defect immediately, assign a status to the result in the Result Details pane. For example, To investigate. 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.

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: