Run Polyspace Analysis on Code Generated from Simulink Model

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

Polyspace Bug Finder™ checks the code for bugs or coding rule violations.
Polyspace Code Prover™ exhaustively checks the code for run-time errors.

This tutorial shows how to run a Polyspace analysis on the code generated from a Simulink model. For the complete 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, in the MATLAB Command Window, run:

openExample('polyspace_code_prover/OpenSimulinkModelForPolyspaceAnalysisExample')

Open Simulink Model for Polyspace Analysis

This example uses:

Open Script

Open the model polyspace_controller_demo.

Generate and Analyze Code

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 list.
Click anywhere in the canvas. The Analyze Code from field shows the model name. Select Run Analysis.

Polyspace starts a Code Prover analysis.

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

Alternatively, in the MATLAB Command Window, enter:

% Load model
load_system('polyspace_controller_demo');
% Generate code
slbuild('polyspace_controller_demo');
% Create Polyspace options object
mlopts = pslinkoptions('polyspace_controller_demo'); 
% Specify result folder
mlopts.ResultDir ='\cp_result';
% Set analysis to Code Prover mode
mlopts.VerificationMode = 'CodeProver'; 
% Run analysis
pslinkrun('polyspace_controller_demo', mlopts);

See pslinkoptions and pslinkrun.

Review Analysis Results

After the analysis is completed, the Polyspace User Interface opens to show the results. The results consist of checks that are color-coded:

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.

Both red checks occur in the handwritten C code in the C Function block Command_Strategy.

Trace and Fix Issues in the Model

Errors in code generated from the model are caused by issues in the model. Trace an error back to your model to investigate the root cause.

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;

The Simulink Editor highlights the origin of this error. In this case, the error occurs due to a transition in the Stateflow chart synch_and_asynch_monitoring. Trace the error to the input variable index of the Stateflow chart.

One possible solution to avoid the orange Out of bounds array index violation is to constrain the input variable index. Use a Saturation block before the Stateflow chart to limit index between zero to 100. After running the analysis on the modified model, the orange check is resolved.

Error 2: Overflow

On the Results List pane, select the orange Overflow error shown in the code here. The error appears in the file polyspace_controller_demo.c.

/* Gain: '<S1>/Gain' incorporates:
* Inport: '<Root>/Battery Info'
* Inport: '<Root>/Rotation'
* Sum: '<S1>/Sum1'
*/

rtb_k = (int16_T)(((int16_T)((in_rotation + in_battery_info) >> 1) * 24576) >>
                   10);

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. The Simulink Editor highlights the origin of this error. In this case, the error occurs in the Fault Management subsystem inside a Gain block following a Sum block.

One possible solution to avoid the orange Overflow error is to constrain the value of the signal in_battery_info that is fed to the Sum block.

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 to a lower value, such as 500.

After running the analysis on the modified model, the orange check is resolved.

The errors in this model occur due to one of these design issues:

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

Start a Bug Finder analysis to check for coding rule violations.

On the Polyspace tab, select Settings > Project Settings and enable the MISRA C:2012 coding standard in the Coding Standards & Code Metrics node. Save the configuration and close the window.
On the Polyspace tab, select Bug Finder.
Click Apply or OK and rerun the analysis.

Alternatively, in the MATLAB Command Window, enter:

% Enable checking for MISRA C:2012 violations
mlopts.VerificationSettings = 'PrjConfigAndMisraC2012';
% Specify separate folder for Bug Finder analysis
mlopts.ResultDir ='\bf_result';
% Set analysis to Bug Finder mode
mlopts.VerificationMode = 'BugFinder'; 
% Run analysis
pslinkrun('polyspace_controller_demo', mlopts);

After the analysis is completed, the Polyspace UI opens containing a list of MISRA C:2012 rule violations.

Annotate Blocks to Justify Results

You can justify your results by adding annotations to your blocks. During code analysis, Polyspace 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'
*/
rtb_k = (int16_T)(((int16_T)((in_rotation + in_battery_info) >> 1) * 24576) >>
                   10);

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.
Regenerate code and rerun the analysis. The Severity and Status columns on the Results List pane are prepopulated with your annotations.