Documentation

Run Verification

Tutorial Overview

In this tutorial, you run verification on your source code. Perform the steps outlined for remote verification if you want to perform verification on another machine. Otherwise, perform the steps outlined for local verification.

Before You Start the Tutorial

Before you start, you must:

Prepare for Verification

If example_project.psprj is not already open in the Project Browser, then:

  1. Select File > Open.

  2. In the Open File dialog box, navigate to polyspace_project.

  3. Select the project file example_project.

  4. Click Open.

Run Remote Verification

Start Verification

Before you start remote verification, you must perform a one-time setup. See Modify Polyspace Server Configuration.

  1. On the Project Browser pane, select Module_1.

  2. On the Configuration pane, select Machine Configuration.

  3. Select Send to Polyspace Server. By default, this action enables the Add to results repository option.

  4. On the toolbar, click .

    The following happens:

    1. On the local host computer, Polyspace Code Prover™ compiles your code.

    2. When the Compile phase is complete, you see the message Verification queued on server in the Output Summary tab.

If the verification fails, go to Troubleshooting in Polyspace Products for Ada.

Monitor Progress

To monitor the progress of a remote verification:

  1. Select Tools > Open Job Monitor.

  2. In the Polyspace Job Monitor, right-click your verification.

  3. Select View Log File.

Stop Verification

To stop a remote verification:

  1. Select Tools > Open Job Monitor.

  2. In the Polyspace Job Monitor, right-click your verification.

  3. Select Remove From Queue.

Run Local Verification

Start Verification

To start a verification on your local computer:

  1. In the Polyspace user interface, in the Project Browser, select Module_1.

  2. On the Configuration pane, select Machine Configuration. Clear Send to Polyspace Server if it is selected.

  3. On the toolbar, click .

If the verification fails, go to Troubleshooting in Polyspace Products for Ada.

Monitor Progress

To monitor the progress of a local verification, on the Output Summary pane, use the following tabs:

  • Output Summary

  • Run Log

    If this window is not visible by default, select Window > Show/Hide View > Run Log.

When the verification is complete, you see:

  • Results on the Results Summary pane.

  • Statistics, such as Code covered by verification and Check Distribution on the Dashboard pane.

Stop Verification

To stop a local verification:

  1. On the toolbar, click .

    A warning dialog box opens.

  2. Click Yes.

    The verification stops. If you restart the verification, it starts from the beginning.

Was this topic helpful?