Annotate Code for Justifying Polyspace Checks

This example shows how to turn on comments in the generated code that suppress error detection through Polyspace®.

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('slbuild(''mSatAddSub'')');

%The generated code is:
file = fullfile('mSatAddSub_ert_rtw','mSatAddSub.c');
coder.example.extractLines(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;
  }

  /* Sum: '<Root>/SubUnsigned' */
  USub = qY;

  /* Outport: '<Root>/Out3' */
  mSatAddSub_Y.Out3 = USub;

  /* Matfile logging */
  rt_UpdateTXYLogVars(mSatAddSub_M->rtwLogInfo, (&mSatAddSub_M->Timing.taskTime0));

  /* signal main to stop simulation */
  {                                    /* Sample time: [1.0s, 0.0s] */
    if ((rtmGetTFinal(mSatAddSub_M)!=-1) &&
        !((rtmGetTFinal(mSatAddSub_M)-mSatAddSub_M->Timing.taskTime0) >
          mSatAddSub_M->Timing.taskTime0 * (DBL_EPSILON))) {
      rtmSetErrorStatus(mSatAddSub_M, "Simulation finished");
    }
  }

  /* Update absolute time for base rate */
  /* The "clockTick0" counts the number of times the code of this task has
   * been executed. The absolute time is the multiplication of "clockTick0"
   * and "Timing.stepSize0". Size of "clockTick0" ensures timer will not
   * overflow during the application lifespan selected.
   */
  mSatAddSub_M->Timing.taskTime0 =
    ((time_T)(++mSatAddSub_M->Timing.clockTick0)) *
    mSatAddSub_M->Timing.stepSize0;
}

/* Model initialize function */
void mSatAddSub_initialize(void)
{
  /* Registration code */

  /* initialize non-finites */
  rt_InitInfAndNaN(sizeof(real_T));

  /* initialize real-time model */
  (void) memset((void *)mSatAddSub_M, 0,
                sizeof(RT_MODEL_mSatAddSub));
  rtmSetTFinal(mSatAddSub_M, 1.0);
  mSatAddSub_M->Timing.stepSize0 = 1.0;

  /* Setup for data logging */
  {
    static RTWLogInfo rt_DataLoggingInfo;
    rt_DataLoggingInfo.loggingInterval = (NULL);
    mSatAddSub_M->rtwLogInfo = &rt_DataLoggingInfo;
  }

  /* Setup for data logging */
  {
    rtliSetLogXSignalInfo(mSatAddSub_M->rtwLogInfo, (NULL));
    rtliSetLogXSignalPtrs(mSatAddSub_M->rtwLogInfo, (NULL));
    rtliSetLogT(mSatAddSub_M->rtwLogInfo, "tout");
    rtliSetLogX(mSatAddSub_M->rtwLogInfo, "");
    rtliSetLogXFinal(mSatAddSub_M->rtwLogInfo, "");
    rtliSetLogVarNameModifier(mSatAddSub_M->rtwLogInfo, "rt_");
    rtliSetLogFormat(mSatAddSub_M->rtwLogInfo, 1);
    rtliSetLogMaxRows(mSatAddSub_M->rtwLogInfo, 1000);
    rtliSetLogDecimation(mSatAddSub_M->rtwLogInfo, 1);

    /*
     * Set pointers to the data and signal info for each output
     */
    {
      static void * rt_LoggedOutputSignalPtrs[] = {
        &mSatAddSub_Y.Out3
      };

      rtliSetLogYSignalPtrs(mSatAddSub_M->rtwLogInfo, ((LogSignalPtrsType)
        rt_LoggedOutputSignalPtrs));
    }

    {
      static int_T rt_LoggedOutputWidths[] = {
        1
      };

      static int_T rt_LoggedOutputNumDimensions[] = {
        1
      };

      static int_T rt_LoggedOutputDimensions[] = {
        1
      };

      static boolean_T rt_LoggedOutputIsVarDims[] = {
        0
      };

      static void* rt_LoggedCurrentSignalDimensions[] = {
        (NULL)
      };

      static int_T rt_LoggedCurrentSignalDimensionsSize[] = {
        4
      };

      static BuiltInDTypeId rt_LoggedOutputDataTypeIds[] = {
        SS_UINT32
      };

      static int_T rt_LoggedOutputComplexSignals[] = {
        0
      };

      static RTWPreprocessingFcnPtr rt_LoggingPreprocessingFcnPtrs[] = {
        (NULL)
      };

      static const char_T *rt_LoggedOutputLabels[] = {
        "USub" };

      static const char_T *rt_LoggedOutputBlockNames[] = {
        "mSatAddSub/Out3" };

      static RTWLogDataTypeConvert rt_RTWLogDataTypeConvert[] = {
        { 0, SS_UINT32, SS_UINT32, 0, 0, 0, 1.0, 0, 0.0 }
      };

      static RTWLogSignalInfo rt_LoggedOutputSignalInfo[] = {
        {
          1,
          rt_LoggedOutputWidths,
          rt_LoggedOutputNumDimensions,
          rt_LoggedOutputDimensions,
          rt_LoggedOutputIsVarDims,
          rt_LoggedCurrentSignalDimensions,
          rt_LoggedCurrentSignalDimensionsSize,
          rt_LoggedOutputDataTypeIds,
          rt_LoggedOutputComplexSignals,
          (NULL),
          rt_LoggingPreprocessingFcnPtrs,

          { rt_LoggedOutputLabels },
          (NULL),
          (NULL),
          (NULL),

          { rt_LoggedOutputBlockNames },

          { (NULL) },
          (NULL),
          rt_RTWLogDataTypeConvert
        }
      };

      rtliSetLogYSignalInfo(mSatAddSub_M->rtwLogInfo, rt_LoggedOutputSignalInfo);

      /* set currSigDims field */
      rt_LoggedCurrentSignalDimensions[0] = &rt_LoggedOutputWidths[0];
    }

    rtliSetLogY(mSatAddSub_M->rtwLogInfo, "yout");
  }

  /* block I/O */

  /* exported global signals */
  USub = 0U;

  /* external inputs */
  U1 = 0U;
  U2 = 0U;

  /* external outputs */
  mSatAddSub_Y.Out3 = 0U;

  /* Matfile logging */
  rt_StartDataLoggingWithStartTime(mSatAddSub_M->rtwLogInfo, 0.0, rtmGetTFinal
    (mSatAddSub_M), mSatAddSub_M->Timing.stepSize0, (&rtmGetErrorStatus
    (mSatAddSub_M)));
}

/* Model terminate function */
void mSatAddSub_terminate(void)
{
  /* (no terminate code required) */
}

/*
 * File trailer for generated code.
 *
 * [EOF]
 */

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 on Operator annotations.

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

6. The generated code is:

file = fullfile('mSatAddSub_ert_rtw','mSatAddSub.c');
coder.example.extractLines(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:operator MISRA2012:D4.1 CERT-C:INT30-C 'Justifying MISRA C rule violation'*/
    /*MW:OvSatOk*/ U2;
  if (qY > U1) {
    qY = 0U;
  }

  /* Sum: '<Root>/SubUnsigned' */
  USub = qY;

  /* Outport: '<Root>/Out3' */
  mSatAddSub_Y.Out3 = USub;

  /* Matfile logging */
  rt_UpdateTXYLogVars(mSatAddSub_M->rtwLogInfo, (&mSatAddSub_M->Timing.taskTime0));

  /* signal main to stop simulation */
  {                                    /* Sample time: [1.0s, 0.0s] */
    if ((rtmGetTFinal(mSatAddSub_M)!=-1) &&
        !((rtmGetTFinal(mSatAddSub_M)-mSatAddSub_M->Timing.taskTime0) >
          mSatAddSub_M->Timing.taskTime0 * (DBL_EPSILON))) {
      rtmSetErrorStatus(mSatAddSub_M, "Simulation finished");
    }
  }

  /* Update absolute time for base rate */
  /* The "clockTick0" counts the number of times the code of this task has
   * been executed. The absolute time is the multiplication of "clockTick0"
   * and "Timing.stepSize0". Size of "clockTick0" ensures timer will not
   * overflow during the application lifespan selected.
   */
  mSatAddSub_M->Timing.taskTime0 =
    ((time_T)(++mSatAddSub_M->Timing.clockTick0)) *
    mSatAddSub_M->Timing.stepSize0;
}

/* Model initialize function */
void mSatAddSub_initialize(void)
{
  /* Registration code */

  /* initialize non-finites */
  rt_InitInfAndNaN(sizeof(real_T));

  /* initialize real-time model */
  (void) memset((void *)mSatAddSub_M, 0,
                sizeof(RT_MODEL_mSatAddSub));
  rtmSetTFinal(mSatAddSub_M, 1.0);
  mSatAddSub_M->Timing.stepSize0 = 1.0;

  /* Setup for data logging */
  {
    static RTWLogInfo rt_DataLoggingInfo;
    rt_DataLoggingInfo.loggingInterval = (NULL);
    mSatAddSub_M->rtwLogInfo = &rt_DataLoggingInfo;
  }

  /* Setup for data logging */
  {
    rtliSetLogXSignalInfo(mSatAddSub_M->rtwLogInfo, (NULL));
    rtliSetLogXSignalPtrs(mSatAddSub_M->rtwLogInfo, (NULL));
    rtliSetLogT(mSatAddSub_M->rtwLogInfo, "tout");
    rtliSetLogX(mSatAddSub_M->rtwLogInfo, "");
    rtliSetLogXFinal(mSatAddSub_M->rtwLogInfo, "");
    rtliSetLogVarNameModifier(mSatAddSub_M->rtwLogInfo, "rt_");
    rtliSetLogFormat(mSatAddSub_M->rtwLogInfo, 1);
    rtliSetLogMaxRows(mSatAddSub_M->rtwLogInfo, 1000);
    rtliSetLogDecimation(mSatAddSub_M->rtwLogInfo, 1);

    /*
     * Set pointers to the data and signal info for each output
     */
    {
      static void * rt_LoggedOutputSignalPtrs[] = {
        &mSatAddSub_Y.Out3
      };

      rtliSetLogYSignalPtrs(mSatAddSub_M->rtwLogInfo, ((LogSignalPtrsType)
        rt_LoggedOutputSignalPtrs));
    }

    {
      static int_T rt_LoggedOutputWidths[] = {
        1
      };

      static int_T rt_LoggedOutputNumDimensions[] = {
        1
      };

      static int_T rt_LoggedOutputDimensions[] = {
        1
      };

      static boolean_T rt_LoggedOutputIsVarDims[] = {
        0
      };

      static void* rt_LoggedCurrentSignalDimensions[] = {
        (NULL)
      };

      static int_T rt_LoggedCurrentSignalDimensionsSize[] = {
        4
      };

      static BuiltInDTypeId rt_LoggedOutputDataTypeIds[] = {
        SS_UINT32
      };

      static int_T rt_LoggedOutputComplexSignals[] = {
        0
      };

      static RTWPreprocessingFcnPtr rt_LoggingPreprocessingFcnPtrs[] = {
        (NULL)
      };

      static const char_T *rt_LoggedOutputLabels[] = {
        "USub" };

      static const char_T *rt_LoggedOutputBlockNames[] = {
        "mSatAddSub/Out3" };

      static RTWLogDataTypeConvert rt_RTWLogDataTypeConvert[] = {
        { 0, SS_UINT32, SS_UINT32, 0, 0, 0, 1.0, 0, 0.0 }
      };

      static RTWLogSignalInfo rt_LoggedOutputSignalInfo[] = {
        {
          1,
          rt_LoggedOutputWidths,
          rt_LoggedOutputNumDimensions,
          rt_LoggedOutputDimensions,
          rt_LoggedOutputIsVarDims,
          rt_LoggedCurrentSignalDimensions,
          rt_LoggedCurrentSignalDimensionsSize,
          rt_LoggedOutputDataTypeIds,
          rt_LoggedOutputComplexSignals,
          (NULL),
          rt_LoggingPreprocessingFcnPtrs,

          { rt_LoggedOutputLabels },
          (NULL),
          (NULL),
          (NULL),

          { rt_LoggedOutputBlockNames },

          { (NULL) },
          (NULL),
          rt_RTWLogDataTypeConvert
        }
      };

      rtliSetLogYSignalInfo(mSatAddSub_M->rtwLogInfo, rt_LoggedOutputSignalInfo);

      /* set currSigDims field */
      rt_LoggedCurrentSignalDimensions[0] = &rt_LoggedOutputWidths[0];
    }

    rtliSetLogY(mSatAddSub_M->rtwLogInfo, "yout");
  }

  /* block I/O */

  /* exported global signals */
  USub = 0U;

  /* external inputs */
  U1 = 0U;
  U2 = 0U;

  /* external outputs */
  mSatAddSub_Y.Out3 = 0U;

  /* Matfile logging */
  rt_StartDataLoggingWithStartTime(mSatAddSub_M->rtwLogInfo, 0.0, rtmGetTFinal
    (mSatAddSub_M), mSatAddSub_M->Timing.stepSize0, (&rtmGetErrorStatus
    (mSatAddSub_M)));
}

/* Model terminate function */
void mSatAddSub_terminate(void)
{
  /* (no terminate code required) */
}

/*
 * File trailer for generated code.
 *
 * [EOF]
 */

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

7. Close the model.

bdclose(model)

Annotate Code for Justifying Polyspace Checks

Polyspace Checks

Code Generation

Related Topics