Quick Start Guide for Polyspace Code Prover
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. It produces results without requiring program execution, code instrumentation, or test cases. Polyspace Code Prover uses semantic analysis and abstract interpretation based on formal methods to verify software interprocedural, control, and data flow behavior. Each operation is color-coded to indicate whether it is free of run-time errors, proven to fail, unreachable, or unproven.
The following steps describe how to run Polyspace on your source code. If you want to skip the project setup and configuration steps:
- Open the demo project. Select Help > Examples > Code_Prover_Example.psprj. You see the results from a Polyspace run.
- To see the demo project, select Window > Reset Layout > Project Setup.
Step 1: Set Up Project
In the Polyspace user interface, select File > New Project.
To add source code for analysis, do one of the following:
- Copy the example files example.c and include.h from MATLAB_Install\polyspace\examples\cxx\Code_Prover_Example\sources to a new folder. Change the read-only status of the files. Add the folder to your project as both source and include folder. MATLAB_Install is the location of your MATLAB installation such as C:\Program Files\MATLAB\R2017a.
- Add your own source code to the project.
Step 2: Configure Project and Run Verification
On the Project Browser pane, select the node below the Configuration node in your project.
The default analysis options appear on the Configuration pane. Retain the default options or change them to your requirements. For example, to check for coding rule violations, select Coding Rules & Code Metrics and specify your options. For more information on an option, place your cursor on the option and select More Help.
Click the Run Code Prover button.
Step 3: Review Results
After verification, the results open on the Results List pane. From the grouping dropdown, select None. Select each result to view the source code location on the Source pane and further information about the result on the Result Details pane. For more information about a result, on the Result Details pane, click the question mark button.
Review each result and determine whether you want to fix your code or add comments justifying the result.