Main Content

Run Polyspace Analysis on Code Generated from Simulink Model

This tutorial shows how to run a Polyspace® analysis on C/C++ code generated from a Simulink® model. You can also analyze C/C++ code generated from a subsystem. 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.

Check for Run-Time Errors in Generated Code

  1. On the Apps tab, select Polyspace Code Verifier. The Polyspace tab opens.

  2. On the Polyspace tab, select Code Prover in the Mode section.

  3. Locate the Analyze section and select Code Generated as Top model from the drop-down list.

  4. Click Run Analysis. Polyspace checks if the model has been changed since the last code generation. If the generated code is up-to-date, Polyspace starts the analysis. If the generated code is not up-to-date or if there is no generated code, Polyspace generates the code first and then starts the analysis.

    A snapshot of a section of the Polyspace tab on the Simulink toolstrip. In this section, you can select which code to analyze and then run analysis.

Alternatively, to start the analysis from 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);
For more information about running Polyspace analysis in the MATLAB Command Window, See pslinkoptions and pslinkrun.

Review Analysis Results

After the analysis completes, the analysis results appear in the Polyspace user interface. The results consist of color coded checks:

  • Green(green tick): The check appear on proven code that does not fail for the data constraints provided. For instance, a division operation does not cause a Division by Zero error.

  • Red(red dot): The check appear on a verified error that always fails for the set of data constraints provided. For instance, a division operation always causes a Division by Zero error.

  • Orange(orange question mark): The check indicates a possible error in unproven code that can fail for certain values of the data constraints provided. For instance, a division operation sometimes causes a Division by Zero error.

  • Gray(gray cross): The check indicates a code operation that cannot be reached for the data constraints provided.

Review each result in detail. In your Code Prover results:

  1. On the Results List pane, locate the red Out of bounds array index check. Click the red check (red dot).

  2. On the Source pane, place your cursor on the red check on the [ operator to view the tooltip. It 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

Issues reported by Polyspace on generated code might be caused by issues in the model. Trace an issue back to your model to investigate the root cause. Issues in code might occur due to a design issue such as:

  • Faulty scaling, unknown calibrations, and untested data ranges coming out of a subsystem into an arithmetic block.

  • Saturations leading to unexpected data flow inside the generated code.

  • Faulty programming in custom code blocks such as the C Function and Stateflow blocks.

To fix design issues in the example model, identify the root cause of run-time errors reported by Polyspace:

Illegally dereferenced pointer

  1. On the Results List pane, select the Illegally dereferenced pointer check.

  2. On the Source pane, click the link <Root>/Command strategy in the comments above the error.

      /* CFunction: '<Root>/Command strategy' incorporates:
   *  DataTypeConversion: '<S3>/Cast4'
   *  Inport: '<Root>/Battery info'
   */
  //...
  p = &array[0];
  for (i = 0; i < 100; i++) {
   *p = 0;
    p = &p[1];
  }
  rtb_x = (int16_T)((uint16_T)rtb_y1 - in_battery_info);
  if (rtb_x < 3) {
    rtb_x = (int16_T)(*p + 5);
  //...

The Simulink Editor highlights the C Function block from which this error arises. In this block, the pointer p is incremented 100 times, pointing *p outside the bound of array. The dereferencing operation in rtb_x = (int16_T)(*p + 5); then causes a red Illegally dereferenced pointer check.

One solution for this error is to point *p to a valid memory location after the for loop in the C Function block:

// After the for loop, point p to a valid memory location
p = &(array[50]);
// ...
tmp = *p + 5;

Out of bounds array index

  1. On the Results List pane, select the Out of bounds array index check.

  2. On the Source pane, click the link <Root>/Command strategy in the comments above the error.

      /* CFunction: '<Root>/Command strategy' incorporates:
   *  DataTypeConversion: '<S3>/Cast4'
   *  Inport: '<Root>/Battery info'
   */
  //...
   for (i = 0; i < 100; i++) {
    *p = 0;
    p = &p[1];
  }
  //...
  if ((rtb_x > 92) && (rtb_x < 110)) {
    if (another_array[(rtb_x - i) + 9] != 0) {
      rtb_x = 92;
    } else {
      rtb_x = 91;
    }
  }

The Simulink Editor highlights the C Function block from which this error arises. In this block, the value of i is set to 100 after the first for loop. The statement if ((rtb_x > 92) && (rtb_x < 110)) limits the possible value of rtb_x to 93..109. In the statement another_array[(rtb_x - i) + 9] != 0, the possible indices for another_array range from 93+9-100 = 2 to 109+9-100 = 18. Because the array another_array has only two elements, the array access in another_array[(rtb_x - i) + 9] results in a red Out of bounds array index run-time check.

One solution for this error is to modify the prevailing conditions on rtb_x so that the expression [(rtb_x - i) + 9] evaluates to 0 or 1.

if ((rtb_x > 91) && (rtb_x < 93)) {
    if (another_array[(rtb_x - i) + 9] != 0) {
      rtb_x = 92;
    } else {
      rtb_x = 91;
    }
  }

Orange checks

The orange checks represent run-time errors that might occur in specific code execution path. Review the orange checks and triage the source of these potential issues. For instance:

  • Division by zero — This orange check is reported twice. One of these checks is reported in the statement rtb_y1 = (int16_T)((int16_T)(10 * 10) / (int16_T)(10 - rtb_x)). To trace the cause of this possible error, click the comment <S6>/Divide. The Simulink Editor highlights the Divide block. In the execution paths where the ÷ input equals zero, the division operation results in a Division by zero error.

    Divide block related to the orange division by zero check is highlighted in the model.

    To resolve this error, check that the ÷ input is not zero. For instance, use the If (Simulink) block and put the Divide block in an If Action Subsystem (Simulink).

    Modified Simulink model that guards against a possible division by zero error.

    The other Division by zero checks can be resolved using similar techniques to check for a zero denominator.

  • Out of bound array index: This orange check is reported on the statement polyspace_controller_demo_Y.FaultTable[*i] = 10;. To trace the root cause of this potential error, click the link S4:76 in the comments above the orange error. The Simulink Editor highlights the Stateflow chart synch_and_asynch_monitoring. Trace the error to the input variable index of the Stateflow® chart.

    Section of Stateflow chart related to the out of bound array index check is highlighted.

    One solution to avoid this check is to constrain the input variable index. Use a Saturation block before the Stateflow chart to limit the value of index from zero to 100.

  • Overflow: Polyspace reports several orange Overflow checks. Resolve these checks by constraining the inputs. For instance, consider the orange Overflow check in the statement rtb_k = (int16_T)(((int16_T)((in_rotation + in_battery_info) >> 1) * 24576) >> 10). To trace the check back to the model, click the link S1/Gain in the comments above the orange check. The Simulink Editor highlights the Gain block in the Fault Management subsystem.

    Block related to the overflow check is highlighted in the model.

    One solution to avoid the orange Overflow check is to constrain the value of the signal in_battery_info that is fed to the Sum block. For instance:

    1. Double-click the Inport block Battery info that provides the input signal in_battery_info to the model.

    2. On the Signal Attributes tab, change the Maximum value of the signal to a lower value, such as 500.

    Use this technique to address similar orange Overflow checks.

Check for Coding Rule Violations

To check for coding rule violations, start a Polyspace Bug Finder™ analysis.

  1. 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.

    A snapshot of the Configuration pane showing the Coding Standards & Code Metrics section.

  2. In the Mode section, select Bug Finder.

  3. 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 completes, the Polyspace UI opens containing a list of MISRA C:2012 rule violations.

Annotate Blocks to Justify Results

To justify Polyspace results, add annotations to your blocks. During code analysis, Polyspace populates the results with your justification. Once you justify a result, you do not have to review it again in subsequent analyses.

  1. On the Results List pane, from the list in the upper-left corner, select File.

  2. 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.

  3. On the Source pane, click the link S1/Sum1 in the 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.

    Sum block related to the MISRA C:2012 violation is highlighted in the model.

  4. 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.

  5. Regenerate code and rerun the analysis. The Severity and Status columns on the Results List pane are now prepopulated with your annotations.

Related Topics