Run Polyspace Code Prover on Desktop

Polyspace^® Code Prover™ is a sound static analysis tool that proves the absence of overflow, divide-by-zero, out-of-bounds array access, and certain other run-time errors in C and C++ source code. A Code Prover analysis produces results without requiring program execution, code instrumentation, or test cases. Code Prover uses semantic analysis and abstract interpretation based on formal methods to determine control flow and data flow in the code. You can use Code Prover on handwritten code, generated code, or a combination of the two. In the analysis results, each operation is color-coded to indicate whether it is free of run-time errors, proven to fail, unreachable, or unproven.

You can run Code Prover on C/C++ code from the Polyspace user interface or using scripts. See:

Run Polyspace in User Interface
If this is your first time using Polyspace, you might want to start from the Polyspace user interface. You can get help from features such as a project setup wizard, assisted configuration and summarized analysis log.
Run Polyspace on Windows or Linux Command Line
Once you set up a project in the Polyspace user interface and complete a few trial runs, you can export the configuration to scripts that you run automatically or on-demand. You can also run a Polyspace analysis directly from the command line in your operating system. You can then save the commands in batch files (Windows) or shell scripts (Linux) for later runs. If you are running Polyspace Server products using continuous integration tools such as Jenkins^®, you can reuse your scripts from the Polyspace desktop products.
Run Polyspace in MATLAB
If you have a MATLAB^® installation, it is particularly easy to write scripts to run a Polyspace analysis. You get all the benefits of scripting in the MATLAB environment, for instance, automatic help on function syntaxes. After analysis, you can create your own visualization of the results using MATLAB graphics and visualization tools.

Example Files

To follow the steps in this tutorial, copy the files example.c and include.h from polyspaceroot\polyspace\examples\cxx\Code_Prover_Example\sources to another folder. Here, polyspaceroot is the Polyspace installation folder, for instance, C:\Program Files\Polyspace\R2020a.

Run Polyspace in User Interface

Open Polyspace User Interface

Double-click the polyspace executable in polyspaceroot\polyspace\bin. Here, polyspaceroot is the Polyspace installation folder, for instance, C:\Program Files\Polyspace\R2020a. See also Installation Folder.

If you set up a shortcut to Polyspace on your desktop or the Start menu in Windows^®, double-click the shortcut.

Add Source Files

To run a verification, you have to create a new Polyspace project. A Polyspace project points to source and include folders on your file system.

On the left of the Start Page pane, click Start a new project. Alternatively, select File > New Project.

After you provide a project name, on the next screens:

Add your source folder.
In this tutorial, add the path to the folder in which you saved the file example.c. Click Next.
Add your include folder.
In this tutorial, add the path to the folder in which you saved the file include.h. This folder can be the same as the previous folder. Click Finish.

After you finish adding your source and include folders, you see a new project on the Project Browser pane. Your source folders are copied to the first module in the project. You can right-click a project to add more folders later. If you add folders later, you must explicitly copy them to a module.

Configure and Run Polyspace

You can change the default options associated with a Polyspace analysis.

Click the Configuration node in your project module. On the Configuration pane, change options as needed. For instance, on the Coding Rules & Code Metrics node, select Check MISRA C:2004.

For more information, see the tooltip on each option. Click the More help link for context-sensitive help on the options.

To start verification, click Run Code Prover in the top toolbar. If the button indicates Bug Finder, click the arrow beside the button to switch to Code Prover.

Follow the progress of verification on the Output Summary window. After the verification, the results open automatically.

Additional Information

See:

Run Polyspace on Windows or Linux Command Line

You can run Code Prover from the Windows or Linux^® command line with batch (.bat) files or shell (.sh) scripts.

Use the polyspace-code-prover command to run a verification.

To save typing the full path to the command, add the path polyspaceroot\polyspace\bin to the Path environment variable on your operating system. Here, polyspaceroot is the Polyspace installation folder, for instance, C:\Program Files\Polyspace\R2024b.

Navigate to the folder where you saved the files (using cd). Enter the following:

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

Here, . indicates the current folder. The options used 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

After verification, the results are saved in the file ps_results.pscp. You can open this file from the Polyspace user interface. For instance, enter the following:

polyspace ps_results.pscp

Instead of specifying comma-separated sources directly on the command line, you can list the sources in a text file (one file per line). Use the option -sources-list-file to specify this text file.

Additional Information

See:

Run Polyspace in MATLAB

Before you run Polyspace from MATLAB, you must link your Polyspace and MATLAB installations. See Integrate Polyspace with MATLAB and Simulink.

To run an analysis, use a polyspace.Project object. The object has two properties:

Configuration: Specify the analysis options such as sources, includes, compiler and results folder using this property.
Results: After analysis, read the analysis results to a MATLAB table using this property.

To run the analysis, use the run method of this object.

To run Polyspace on the example file example.c in polyspaceroot\polyspace\examples\cxx\Code_Prover_Examples\sources, enter the following at the MATLAB command prompt.

proj = polyspace.Project

% Configure analysis
proj.Configuration.Sources = {fullfile(polyspaceroot, 'polyspace', 'examples',...
    'cxx', 'Code_Prover_Example', 'sources', 'example.c')};
proj.Configuration.EnvironmentSettings.IncludeFolders = {fullfile(polyspaceroot,...
 'polyspace', 'examples', 'cxx', 'Code_Prover_Example', 'sources')};
proj.Configuration.TargetCompiler.Compiler = 'gnu4.9';
proj.Configuration.ResultsDir = fullfile(pwd,'results');
proj.Configuration.CodeProverVerification.MainGenerator = true;


% Run analysis
cpStatus = proj.run('codeProver');

% Read results
resObj = proj.Results;
cpSummary = getSummary(resObj, 'runtime');
cpResults = getResults(resObj, 'readable');

After verification, the results are saved in the file ps_results.pscp. You can open this file from the Polyspace user interface. For instance, enter the following:

resultsFile = fullfile(proj.Configuration.ResultsDir,'ps_results.pscp');
polyspaceCodeProver(resultsFile)

Additional Information

See: