MATLAB Examples

Verify Generated Code Using Polyspace Code Prover

If you generate C or C++ code from models using Embedded Coder, you can check the generated code for run-time errors. Polyspace Code Prover proves code correctness, finds run-time errors, and checks for MISRA-C compliance in generated and handwritten code.

This example contains a demo model from which you can generate code and then analyze the generated code.

Contents

Open Model

Open and explore the example model. The model contains a controller subsystem, which itself contains many subsystems. One of the subsystems has some issues that can lead to run-time errors in the generated code.

open_system('psdemo_model_link_sl');

Generate and Analyze Code

Generate code from the controller subsytem or one of the subsystems underneath. Then, run Polyspace Code Prover on the generated code. You can trace back from run-time errors found in the generated code to corresponding blocks in the model. You can also check for coding rule violations and add annotations on blocks to justify the violations. For details, see docid:codeprover_ug.mw_df3e88d3-f8b0-4b89-b923-1cbdf770a02f.

The controller subsystem also contains an S-Function block. You can separately analyze the C code that the S-Function block refers to. For details, see docid:codeprover_ug.bu582ic.