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
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);
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 signalin_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);
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 functionpolyspace_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:
Select the block. On the Polyspace tab, select Add Annotation.
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.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.