Run Polyspace Code Prover on Server and Upload Results to Web Interface

Polyspace^® Code Prover™ Server™ proves the absence of run-time errors in C/C++ code.

You can run Code Prover as part of continuous integration. Set up scripts that run a Code Prover analysis at regular intervals or based on new submissions. The scripts can upload the analysis results for review in the Polyspace web interface and optionally send emails to owners of source files with Polyspace findings. The owners can open the web interface with only the new findings from their submission, and fix or justify the issues.

In a typical project or team, Polyspace Code Prover Server runs periodically on a few testing servers and uploads the results for review. Each developer and quality engineer in the team has a Polyspace Code Prover Access™ license to view the results in the web interface for further investigation and bug fixing.

Prerequisites

To run a Code Prover analysis on a server and review the results in the Polyspace Code Prover Access web interface, you must perform a one-time setup.

To run the analysis, you must install one instance of the Polyspace Code Prover Server product.
To upload results, you must set up the components required to host the web interface of Polyspace Code Prover Access.
To view the uploaded results, you (and each developer reviewing the results) must have one Polyspace Code Prover Access license.

See Install Polyspace Server and Access Products.

Check Polyspace Installation

To check if Polyspace Code Prover Server is installed:

Open a command window. Navigate to polyspaceserverroot\polyspace\bin (using cd). Here, polyspaceserverroot is the Polyspace Code Prover Server installation folder, for instance, C:\Program Files\Polyspace Server\R2019a.
Enter the following:
polyspace-code-prover-server -help

You should see the list of options allowed for a Code Prover analysis.

To check if the Polyspace web interface is set up for upload:

Navigate again to polyspaceserverroot\polyspace\bin.
Enter the following:
polyspace-access -host hostName -port portNumber -create-project testProject
Here, hostName is the name of the server hosting the Polyspace Code Prover Access web server. For a locally hosted server, use localhost. portNumberI is the optional port number of the server. If you omit the port number, 9443 is used.
If the connection is successful, a project called testProject should be created in the Polyspace web interface.
You are prompted for your login and password each time you use the polyspace-access command. To avoid entering login information each time, you can provide the login and an encrypted version of your password with the command. To create an encrypted password, enter:
polyspace-access -encrypt-password
Enter your login and password. Copy the encrypted password and provide this encrypted password with the -encrypted-password option when using the polyspace-access command.
Open this URL in a web browser:
```
https://hostName:portNumber/metrics/index.html
```
Here, hostName and portNumber are the host name and port number from the previous step.

In the PROJECT EXPLORER pane on the Polyspace web interface, you should see the newly created project testProject.

Run Code Prover on Sample Files

To run Code Prover, open a command window in your operating system.

Use the polyspace-code-prover-server command to run a Code Prover analysis.
Use the polyspace-access command to upload the results to the Polyspace web interface.

To save typing the full path to the command, add the path polyspaceserverroot\polyspace\bin to the Path environment variable on your operating system.

Try out the commands on sample files provided with your Polyspace installation.

Copy the sample source files from polyspaceserverroot\polyspace\examples\cxx\Code_Prover_Example\sources to another folder where you have write permissions. Navigate to this folder (using cd).

Enter the following:

polyspace-code-prover-server -sources example.c,single_file_analysis.c -I . -main-generator -results-dir .
polyspace-access -host hostName -port portNumber -login username -encrypted-password pwd -create-project testProject
polyspace-access -host hostName -port portNumber -login username -encrypted-password pwd -upload . -project myFirstProject -parent-project testProject

Here, username is your login name and pwd is the encrypted password that you created previously. See Check Polyspace Installation.

Refresh the Polyspace web interface. You should see the newly uploaded results under the testProject folder in the PROJECT EXPLORER pane.

To see the results in the project, click Review. For more information, see Polyspace Code Prover Access documentation. You can also access the documentation using the button in the upper right of the Polyspace Access interface.

For the full list of options available for a Code Prover analysis, see Analysis Options. To open the Code Prover documentation in a help browser, enter:

polyspace-code-prover-server -doc

Sample Scripts for Code Prover Analysis on Servers

Instead of typing the commands at the command line, you can write scripts to run the analysis. The scripts can execute each time you add or modify source files.

A sample Windows^® batch file with the previous commands is shown below. Here, the path to the Polyspace installation is specified in the script. To use this script, replace polyspaceserverroot with the path to your installation. You must have generated the encrypted password for use in the scripts. See Check Polyspace Installation.

echo off
set POLYSPACE_PATH=polyspaceserverroot\polyspace\bin
set LOGIN=-host hostName -port portNumber -login username -encrypted-password pwd
"%POLYSPACE_PATH%\polyspace-code-prover-server" -sources example.c,single_file_analysis.c -I .^
 -main-generator -results-dir .
"%POLYSPACE_PATH%\polyspace-access" %LOGIN% -create-project testProject
"%POLYSPACE_PATH%\polyspace-access" %LOGIN% -upload . -project myFirstProject -parent-project testProject
pause

A sample Linux^® shell script with the previous commands is shown below.

POLYSPACE_PATH=polyspaceserverroot/polyspace/bin
LOGIN=-host hostName -port portNumber -login username -encrypted-password pwd
${POLYSPACE_PATH}/polyspace-code-prover-server -sources example.c,single_file_analysis.c -I .\
 -main-generator -results-dir .
${POLYSPACE_PATH}/polyspace-access $LOGIN -create-project testProject
${POLYSPACE_PATH}/polyspace-access $LOGIN -upload . -project myFirstProject -parent-project testProject

Specify Sources and Options in Separate Files from Launching Scripts

Instead of listing the source files and analysis options within the launching scripts, you can list them in separate text files.

You specify the text file listing the sources by using the option -sources-list-file.
You specify the text file listing the analysis options by using the option -options-file.

By removing the source files and analysis option specifications from the launching scripts, you can modify these specifications as required with new code submissions while keeping the launching script untouched.

In the preceding example, you can modify the polyspace-code-prover-server command to use these text files. Instead of:

polyspace-code-prover-server -sources example.c,single_file_analysis.c -I . -main-generator -results-dir .

Use:

polyspace-code-prover-server -sources-list-file sources.txt -options-file polyspace_opts.txt -results-dir .

Here:

sources.txt lists the source files:
```
example.c
single_file_analysis.c
```
polyspace_opts.txt lists the analysis options in separate lines:
```
-I .
-main-generator
```

Typically, your source files are specified in a build command (makefile). Instead of specifying the source files directly, you can trace the build command to create a list of source specifications. See polyspace-configure.

Complete Workflow

In a typical continuous integration workflow, you run a script that executes these steps:

Extract Polyspace options from your build command.
For instance, if you use makefiles to build your source code, you can extract analysis options from the makefile.
polyspace-configure -output-options-file compile_opts make
See also:
- polyspace-configure
- Create Polyspace Analysis Configuration from Build Command
Run the analysis with the previously created options file. Append a second options file with the remaining options required for the analysis.
polyspace-code-prover-server -options-file compile_opts -options-file run_opts
See Prepare Scripts for Polyspace Analysis.

Upload the results to Polyspace Code Prover Access.

polyspace-access login -upload resultsFolder -project projName -parent-project parentProjName

Here, login is the combination of options required to communicate with the web server hosting Polyspace Code Prover Access:

-host hostName -port portNumber -login username -encrypted-password pwd

resultsFolder is the folder containing the Polyspace results. projName and parentProjName are names of the project and parent folder as they would appear in the Polyspace Code Prover Access web interface.

Optionally, send e-mail notifications to developers with new results from their submission. The email contains attachments with links to the results in the Polyspace Code Prover Access web interface.
See Send E-mail Notifications with Polyspace Code Prover Results.

See examples of scripts executing these steps in Sample Scripts for Polyspace Analysis with Jenkins.