Main Content

Run Polyspace Code Prover in Polyspace Platform User Interface

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 Platform user interface or using scripts. See:

  • Run Polyspace in the Polyspace Platform User Interface

    If this is your first time using Polyspace, you might want to start from the Polyspace Platform 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 the Polyspace Platform User Interface

Open the Polyspace Platform User Interface

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

If you open the old desktop user interface and have not set the Polyspace Platform user interface as your default user interface, click the Try the new desktop UI button and optionally select the checkbox to make Polyspace Platform user interface the new default user interface.

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 an analysis, 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 New Project. Alternatively, select New > Project in the taskbar.

Select a location to save your project and enter your project name. Continue by adding your source and include folders. Select Add Source Folder from the taskbar and navigate to your source files folder. In this tutorial, add the folder in which you saved the source and include files.

Your new project is in the Projects pane. Your source folders are added to the Code node in the project. You can add more files or folders later from the right-click context menu or the buttons in the taskbar.

Later, you can group your projects by saving them to a workspace. A workspace allows you to group related projects and open all the projects at once. For more information on how to use workspaces, see Manage Related Projects in Polyspace Platform User Interface Using Workspaces.

Configure and Run Polyspace

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

Double click the Configuration node in the Projects pane. On the Configuration pane, change options as needed. For this tutorial, suppose you want to specify the list of tasks to be analyzed. On the Static Analysis tab, select Multitasking and then select the option Configure multitasking manually. You can then add your tasks to analyze to the corresponding list by either manually entering the task, or by adding a function from a list predefined by Polyspace.

The Configuration pane with Configure multitasking manually selected and the tasks of proc1 and proc2 entered in the Tasks table.

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

Option tooltip for the Use custom checkers file option

Select the Project tab to return to your project toolstrip. To start an analysis, in the Run section of the toolstrip, click Prove Absence of RTEs. The Prove Absence of RTEs button shares a drop down menu with the Find Defects button.

A pane opens so you can follow the progress of analysis. After the analysis, your results show in the Results pane. Double-click the result file to open your results dashboard.

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:

Related Topics