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.
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.
To check if Polyspace Code Prover Server is installed:
Open a command window. Navigate to
.
Here, polyspaceserverroot
\polyspace\bin
is the Polyspace
Code Prover Server installation folder, for instance, polyspaceserverroot
C:\Program
Files\Polyspace Server\R2019a
. 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,
is the
name of the server hosting the Polyspace
Code Prover Access web server. For a locally hosted server, use
hostName
localhost
.
I is the
optional port number of the server. If you omit the port number,
portNumber
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
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
.
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
to the polyspaceserverroot
\polyspace\binPath
environment variable on your operating system.
Try out the commands on sample files provided with your Polyspace installation.
Copy the sample source files from
to another folder where you have write permissions. Navigate to this
folder at the command line. polyspaceserverroot
\polyspace\examples\cxx\Code_Prover_Example\sources
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,
is your
login name and username
is the
encrypted password that you created previously. See Check Polyspace Installation.pwd
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.
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
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 |
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
.
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:
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 |
Upload the results to Polyspace Code Prover Access.
polyspace-access login -upload resultsFolder -project projName -parent-project parentProjName |
Here,
is the
combination of options required to communicate with the web server that
is hosting Polyspace
Code Prover Access:login
-host hostName -port portNumber -login username -encrypted-password pwd |
is the folder containing the Polyspace results.
resultsFolder
and
projName
are
names of the project and parent folder as they would appear in the
Polyspace
Code Prover Access web interface.parentProjName
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 Results.
See examples of scripts executing these steps in Sample Scripts for Polyspace Analysis with Jenkins.
polyspace-access
| polyspace-code-prover-server