Polyspace チェックを正当化するためのコードへの注釈付け

この例では、Polyspace® によるエラー検出を抑制する生成コード内のコメントをオンにする方法を示します。

Polyspace チェック

Polyspace Code Prover™ ソフトウェアを使用すると、Embedded Coder® で生成されたコードに Polyspace 検証を適用できます。生成コードのランタイム エラーが検出され、モデルの不備の特定と修正に役立ちます。Polyspace では、コード ジェネレーターによる特定の演算の実装方法が原因で、それらの演算の適正なオーバーフローが強調表示されることがあります。こうした適正なオーバーフローは、Polyspace によってフラグが設定されないようにする必要があります。このエラー検出を抑制するコード内のコメントを生成します。

コード生成

1. Simulink® モデル例 mSatAddSub を開きます。

model='mSatAddSub';
open_system(model);

2. Embedded Coder アプリの [コンフィギュレーション パラメーター] ダイアログ ボックスで、[演算子の注釈] をオフにします。

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

3. モデルをビルドしてコードを生成するには、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. Polyspace チェックを実行します。コード ジェネレーターで、最大の組み込みデータ型が 32 ビットであることが認識されます。0U とより大きなシングルワードの整数データ型を使用して減算のすべての結果を飽和させることはできません。代わりに、結果のオーバーフローとオーバーフローの方向が検出され、結果が飽和します。飽和を認識できないため、Polyspace によって演算にフラグが設定されます。

5. Embedded Coder アプリの [コンフィギュレーション パラメーター] ダイアログ ボックスで、[演算子の注釈] をオンにします。

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

6. 生成コードは次のようになります。

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]
 */

コード ジェネレーターは、Polyspace によって検出されたエラーを抑制する /*MW:OvSatOk*/ コメントを挿入します。

7. モデルを閉じます。

bdclose(model)

参考

トピック

• モデル コンフィギュレーション パラメーター: コメント
• Embedded Coder によって生成されたコードに対する Polyspace 解析の実行 (Polyspace Bug Finder)