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, and then uploads findings to a web interface for code review.

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 code 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 to review only the new findings from their submission, and then 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 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, perform this one-time setup:

To run the analysis, install one instance of the Polyspace Code Prover Server product.
To upload results, 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 a 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. Here, polyspaceserverroot is the Polyspace Code Prover Server installation folder, for instance, C:\Program Files\Polyspace Server\R2021a. See also Installation Folder.
Enter:
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:
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 setup was complete, a project called testProject is 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, 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.
In a web browser, open this URL:
```
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, in your operating system, open a command window.

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

To avoid 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 at the command line.

Enter:

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 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.

The options used with the polyspace-code-prover-server command are:

-sources: Specify comma-separated source files.
-I: Specify path to include folder. Use the -I flag each time you want to add a separate include folder.
-results-dir: Specify the path to the folder where Polyspace Code Prover results will be saved.
Note that the results folder is cleaned up and repopulated at each run. To avoid accidental removal of files during the cleanup, instead of using an existing folder that contains other files, specify a dedicated folder for the Polyspace results.
Verify module or library (-main-generator): Specify that a main function must be generated if not found in the source files

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

polyspace-code-prover-server -doc

Sample Scripts for Code Prover Analysis on Servers

To run the analysis, instead of typing the commands at the command line, you can use scripts. The scripts can execute each time that you add or modify source files.

A sample Windows^® batch file 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 already 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 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.

Specify the text file listing the sources by using the option -sources-list-file.
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 leaving the launching script untouched.

Consider the script in the preceding example. You can modify the polyspace-code-prover-server command to use text files with sources and options. 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 (Polyspace Code Prover).

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 that contains 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 that is 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 email notifications to developers with new results from their code submission. The email contains attachments with links to the results in the Polyspace Code Prover Access web interface.
See Send Email Notifications with Polyspace Code Prover Server Results.