Run Polyspace Analysis on Code Generated from Simulink Model

This example uses:

You can run Polyspace^® on the code generated from a Simulink^® model or subsystem.

Polyspace Bug Finder™ checks the code for bugs or coding rule violations (for instance, MISRA C^®: 2012 rules).
Polyspace Code Prover™ exhaustively checks the code for run-time errors.

If you use Embedded Coder^® for code generation, this tutorial shows how to run Polyspace on the code generated from a simple Simulink model. For the full workflow, see Run Polyspace Analysis on Code Generated with Embedded Coder.

Prerequisites

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

To open the model used in this example, at the MATLAB Command Window, run:

openExample('polyspace_code_prover/OpenModelForCodeGenerationAndPolyspaceAnalysisExample')

Open Model for Code Generation and Polyspace Analysis

This example uses:

Open Model

Open the model polyspace_controller_demo for configuring code generation and Polyspace analysis.

Generate and Analyze Code

To start the Polyspace analysis of code generated from the model:

On the Apps tab, select Polyspace Code Verifier.
On the Polyspace tab, locate the Analyze field and select Code Generated as Top model from the drop-down menu.
Click anywhere on the canvas. The Analyze Code from field shows the model name. Select Run Analysis.

Polyspace checks for generated code when you click Run Analysis. If no generated code is present, Polyspace first generates the code by using Embedded Coder and then starts the analysis.

Equivalent MATLAB Code:

load_system('polyspace_controller_demo');
slbuild('polyspace_controller_demo');
mlopts = pslinkoptions('polyspace_controller_demo'); 
mlopts.ResultDir ='\result'
mlopts.VerificationMode = 'CodeProver'; 
pslinkrun('polyspace_controller_demo', mlopts);

To analyze with Bug Finder, replace CodeProver with BugFinder. For more information on the code, see pslinkoptions and pslinkrun.

Review Analysis Results

After analysis, the results are displayed in the Polyspace user interface.

If you run Bug Finder, the results consist of bugs detected in the generated code. If you run Code Prover, the results consist of checks that are color-coded as follows:

Green (proven code): The check does not fail for the data constraints provided. For instance, a division operation does not cause a Division by Zero error.
Red (verified error): The check always fails for the set of data constraints provided. For instance, a division operation always causes a Division by Zero error.
Orange (possible error): The check indicates unproven code and can fail for certain values of the data constraints provided. For instance, a division operation sometimes causes a Division by Zero error.
Gray (unreachable code): The check indicates a code operation that cannot be reached for the data constraints provided.

Review each analysis result in detail. For instance, in your Code Prover results:

On the Results List pane, select the red Out of bounds array index check.
On the Source pane, place your cursor on the red check to view additional information. For instance, the tooltip on the red [ operator states the array size and possible values of the array index. The Result Details pane also provides this information.

The error occurs in a handwritten C file Command_strategy_file.c. The C file is inside an S-function block Command_Strategy in the Reduced Precision subsystem (in a model reference relative threshold).

Trace Errors Back to Model and Fix Them

For code generated from the model, you can trace an error back to your model. These sections show how to trace specific Code Prover results back to the model.

Error 1: Out of bounds array index

On the Results List pane, select the orange Out of bounds array index error that occurs in the file polyspace_controller_demo.c.

On the Source pane, click the link S4:76 in comments above the orange error.

/* Transition: '<S4>:75' */
/* Transition: '<S4>:76' */
(*i)++;

/* Outport: '<Root>/FaultTable' */
polyspace_controller_demo_Y.FaultTable[*i] = 10;

You see that the error occurs due to a transition in the Stateflow chart synch_and_asynch_monitoring. You can trace the error to the input variable index of the Stateflow chart.

You can avoid the Out of bounds array index in several ways. One way is to constrain the input variable index using a Saturation block before the Stateflow chart.

Error 2: Overflow

On the Results List pane, select the orange Overflow error shown below. The error appears in the file polyspace_controller_demo.c.
On the Source pane, review the error. To trace the error back to the model, click the link S1/Gain in comments above the orange error.
```
/* Gain: '<S1>/Gain' incorporates:
* Inport: '<Root>/Battery Info'
* Inport: '<Root>/Rotation'
* Sum: '<S1>/Sum1'
*/

Gain = (int16_T)(((int16_T)((in_rotation + in_battery_info) >> 1) * 24576) >>
                   10);
```
You see that the error occurs in the Fault Management subsystem inside a Gain block following a Sum block.

You can avoid the Overflow in several ways. One way is to constrain the value of the signal in_battery_info that is fed to the Sum block. To constrain the signal:

Double-click the Inport block Battery info that provides the input signal in_battery_info to the model.
On the Signal Attributes tab, change the Maximum value of the signal.

The errors in this model occur due to one of the following:

Faulty scaling, unknown calibrations and untested data ranges coming out of a subsystem into an arithmetic block.
Array manipulation in Stateflow event-based modelling and handwritten lookup table functions.
Saturations leading to unexpected data flow inside the generated code.
Faulty Stateflow programming.

Once you identify the root cause of the error, you can modify the model appropriately to fix the issue.

Check for Coding Rule Violations

To check for coding rule violations, before starting code analysis:

On the Polyspace tab, select Settings.
In the Configuration Parameters dialog box, select an appropriate option in the Settings from list. For instance, select Project configuration and MISRA C 2012 AGC Checking.
It is recommended that you run Bug Finder for checking MISRA C:2012 rules. On the Polyspace tab, select Bug Finder.
Click Apply or OK and rerun the analysis.

Annotate Blocks to Justify Results

You can justify your results by adding annotations to your blocks. During code analysis, Polyspace Code Prover reads your annotations and populates the result with your justification. Once you justify a result, you do not have to review it again.

On the Results List pane, from the drop-down list in the upper left corner, select File.
In the file polyspace_controller_demo.c, in the function polyspace_controller_demo_step(), select the violation of MISRA C:2012 rule 10.4. The Source pane shows that an addition operation violates the rule.
On the Source pane, click the link S1/Sum1 in comments above the addition operation.
```
/* Gain: '<S1>/Gain' incorporates:
* Inport: '<Root>/Battery Info'
* Inport: '<Root>/Rotation'
* Sum: '<S1>/Sum1'
*/
Gain = (int16_T)(((int16_T)((in_rotation + in_battery_info) >> 1) * 24576) >>
                   10);
```
You see that the rule violation occurs in a Sum block.
To annotate this block and justify the rule violation:
1. Select the block. On the Polyspace tab, select Add Annotation.
2. Select MISRA-C-2012 for Annotation type and enter information about the rule violation. Set the Status to No action planned and the Severity to Unset.
3. Click Apply or OK. The words Polyspace annotation appear below the block, indicating that the block contains a code annotation.
4. Regenerate code and rerun the analysis. The Severity and Status columns on the Results List pane are prepopulated with your annotations.