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.
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, look for this example in the MATLAB Help browser and click the Open Model button.
Open the model polyspace_controller_demo
for configuring code generation and Polyspace analysis.
To generate code from the model, on the Apps tab, select Embedded Coder. On the C Code tab, select Generate Code.
Equivalent MATLAB Code:
load_system('polyspace_controller_demo'); rtwbuild('polyspace_controller_demo');
To analyze the code generated from the model, on the Apps tab, select Polyspace Code Verifier. On the Polyspace tab:
Select the product to run: Bug Finder or Code Prover.
Click anywhere on the canvas. The Analyze Code from field shows the model name. Select Run Analysis.
Equivalent MATLAB Code:
mlopts = pslinkoptions('polyspace_controller_demo'); mlopts.ResultDir ='\result' mlopts.VerificationMode = 'CodeProver'; pslinkrun('polyspace_controller_demo', mlopts);
CodeProver
with
BugFinder
. For more information on the code, see pslinkoptions
and pslinkrun
.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
).
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.
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.
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);
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.
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.
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:
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.