Polyspace Verification of C/C++ Code Generated by MATLAB Coder

To check for run-time errors in C/C++ code generated from MATLAB^® code, you can use Polyspace^® Code Prover™. To check for defects, you can use Polyspace Bug Finder™. If you have Polyspace and Embedded Coder^®, Polyspace is integrated into the MATLAB Coder™ workflow.

In the MATLAB Coder app, you can run Polyspace analysis without additional setup.
At the command line, after code generation with codegen, you can run Polyspace analysis on the generated code by providing the code generation output folder to pslinkrun (Polyspace Bug Finder).

Run Polyspace Analysis in the MATLAB Coder App

Generate standalone C/C++ code (a static library, dynamically linked library, or executable program).
On the Generate Code page, click Polyspace.
Select the options. See Configure Advanced Polyspace Options in MATLAB Coder App (Polyspace Code Prover).
Click Run.
The app logs the analysis output on the Polyspace Log tab and opens the Polyspace user interface.

Run Polyspace Analysis on Code Generated by `codegen`

Create a pslinkoptions object for verification of code generated by MATLAB Coder.
As needed, change object properties:
- In the ResultDir property, specify the name of the folder for the Polyspace results.
- In the VerificationMode property, specify the Polyspace verification product.
Run the verification by using pslinkrun. Provide the pslinkoptions object and the folder that contains the generated code.
To view verification results, open the Polyspace user interface.

For example, suppose that you generated a static library for the MATLAB function myFunction and that the code generation output folder is codegen/lib/myFunction. To run Polyspace Code Prover on the generated code, use this code:

opts = pslinkoptions('codegen');
opts.ResultDir = 'polyspace';
opts.VerificationMode = 'CodeProver';
pslinkrun('-codegenfolder', 'codegen/lib/myFunction', opts);
polyspaceCodeProver('polyspace/myFunction.psprj');

You can also set the VerificationMode property to 'BugFinder' and view verification results by using polyspaceBugFinder.

Review Analysis Results

In the Results List pane of the Polyspace user interface, review the run-time checks. See whether you can trace the issues back to the original MATLAB code. See Interactively Trace Between MATLAB Code and Generated C/C++ Code.

For example, an operation in the C code might overflow because Polyspace assumes an unbounded range for a function input. Consider specifying a constraint on the input and reanalyzing the code with Polyspace. See Run Polyspace on C/C++ Code Generated from MATLAB Code (Polyspace Code Prover).