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 Access™ license to view the results in the web interface for investigation and bug fixing.

Diagram of continuous integration workflow using Polyspace products

Prerequisites

To run a Code Prover analysis on a server and review the results in the Polyspace 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 Access.
To view the uploaded results, you and each developer reviewing the results must have a Polyspace 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\R2024b. 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 Access web server. For a locally hosted server, use localhost. portNumber 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 (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><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.

Polyspace Access Project Explorer

To see the results in the project, click Review. For more information, see Review Polyspace Code Prover Results in Web Browser. 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 Complete List of Polyspace Code Prover Analysis Options. To open the Code Prover documentation in your system web 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.

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. The command below first executes make and then determines the analysis options from the processes executed.
```
polyspace-configure -output-options-file compile_opts make
```
See also:
- polyspace-configure
- Create Polyspace Analysis Configuration from Build Command (Makefile)
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 Specifying Multiple Options Files.
Upload the results to Polyspace 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 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 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 Access web interface.
See Send Email Notifications with Polyspace Code Prover Server Results.

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