Polyspace Checks

With the Polyspace Code Prover software you can apply Polyspace verification to Embedded Coder generated code. The software detects run-time errors in the generated code and helps you to locate and fix model faults. Polyspace might highlight overflows for certain operations that are legitimate because of the way the code generator implements these operations. These legitimate overflows should not be flagged by Polyspace. Generate comments in the code that suppress this error detection.

Code Generation

1. Open the example Simulink model mSatAddSub.

model='mSatAddSub';
open_system(model);

2. In the Embedded Coder app on the Configuration Parameters dialog box, turn off Operator annotations.

set_param('mSatAddSub','OperatorAnnotations','off');

3. To build the model and generate code, press Ctrl+B.

evalc('rtwbuild(''mSatAddSub'')');

%The generated code is:
file = fullfile('mSatAddSub_ert_rtw','mSatAddSub.c');
rtwdemodbtype(file,'/* Model step function */',...
    'End of Sum',1,1);

/* Model step function */
void mSatAddSub_step(void)
{
  uint32_T qY;

  /* Sum: '<Root>/SubUnsigned' incorporates:
   *  Inport: '<Root>/In1'
   *  Inport: '<Root>/In2'
   */
  qY = U1 - U2;
  if (qY > U1) {
    qY = 0U;
  }

  USub = qY;

4. Run the Polyspace check. The code generator recognizes that the largest built-in data type is 32-bit. It is not possible to saturate all the results of the subtractions using 0U and a bigger single-word integer data type. Instead the software detects the results overflow and the direction of the overflow, and saturates the result. The operation is flagged by Polyspace because it fails to recognize the saturation.

5. In the Embedded Coder app on the Configuration Parameters dialog box, turn off Operator annotations.

set_param('mSatAddSub','OperatorAnnotations',"on");
evalc('rtwbuild(''mSatAddSub'')');

6. The generated code is:

file = fullfile('mSatAddSub_ert_rtw','mSatAddSub.c');
rtwdemodbtype(file,'/* Model step function */',...
    'End of Sum',1,1);

/* Model step function */
void mSatAddSub_step(void)
{
  uint32_T qY;

  /* Sum: '<Root>/SubUnsigned' incorporates:
   *  Inport: '<Root>/In1'
   *  Inport: '<Root>/In2'
   */
  qY = U1 - /*MW:OvSatOk*/ U2;
  if (qY > U1) {
    qY = 0U;
  }

  USub = qY;

The code generator inserts the /*MW:OvSatOk*/ comment that suppresses the error detected by Polyspace.

7. Close the model.

bdclose(model)
rtwdemoclean;