Documentation

Review Verification Results

Tutorial Overview

In this tutorial, you explore the results of verifying example.c. Before starting this tutorial, complete Run Verification.

Open Results

Remote Verification

To open results from a remote verification:

  1. Select Metrics > Open Metrics.

    Alternatively, you can enter the remote address directly in a web browser. For more information, see View Polyspace Metrics Project Index.

  2. Click the Project cell of your verification.

    You can see a summary of your project.

  3. On the Summary tab, click the 1.0 cell in the Verification column.

    Your results are downloaded into the user interface.

Local Verification

After verification, the results open automatically.

Review Results

Polyspace® performs checks on each operation in your code. The software reports whether a check is green, red, orange or gray.

Check colorIndicates
Red The code operation fails the check on every execution path.
GreenThe code operation passes the check on every execution path.
OrangeThe code operation fails the check on some execution paths.
GrayThe code operation is unreachable from entry-point functions.

  1. On the Results Summary pane, select Group by > File.

    The checks are grouped by file. Within each file, the checks are grouped by function.

  2. Expand the following function names and select a check in the function. The corresponding line of code on the Source pane appears highlighted.

    Function CheckSource Code AppearanceReason
    UNREACHABLE_CODEGray Unreachable codeThe : on line 182 is gray. x is greater than 0. So the if statement branch cannot be reached.
    INFINITE_LOOPRed Non-terminating loopThe keyword loop on line 123 is red.x cannot be less than 0. So the code cannot exit the loop.
    RECURSIONOrange Division by Zero The / sign on line 62 is orange.The denominator can be zero.
    NON_INFINITE_LOOPGreen OverflowThe + sign on line 112 is green.cur does not overflow. The loop on line 110 terminates before cur can overflow.

  3. To find further information about a check, do one of the following:

    • View the message on the Result Details pane.

    • Place your cursor on the check in the Source pane. View the tooltip.

  4. Filter Division by Zero checks. To do this:

    1. Click on the Check column header.

    2. From the drop-down list, clear All and select Division by Zero.

    The Results Summary pane displays only the Division by Zero checks.

  5. On the Results Summary pane, select the red Division by Zero check in the function PROCEDURE_ZDV. Enter the following review information.

    ColumnAction
    SeverityHigh
    StatusFix
    Commentx is always zero

Generate Report

To generate a verification report:

  1. If your verification results are not already open, open them.

  2. Select Reporting > Run Report.

  3. In the Select Reports section, select Developer.

  4. For Output folder, select C:\polyspace_project\Module_1\Result_1\Polyspace-Doc.

  5. For Output format, select PDF .

  6. Click Run Report.

    The software creates the specified report and opens it.

Was this topic helpful?