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

この例では、静的コード解析中に Embedded Coder® が生成されたコード内の演算子の注釈を使用して、特定の算術演算を正当化し、Polyspace 調査結果を非表示にする方法を示します。

Polyspace Code Prover™ を使用すると、Embedded Coder によって生成されたコードに対して Polyspace 静的検証を実行できます。Polyspace は、生成されたコード内のランタイム エラーを検出し、モデル化の欠陥の特定を支援します。場合によっては、コード ジェネレーターでの実装方法が原因で、設計上は安全な演算のオーバーフローを Polyspace が報告することがあります。このような調査結果はエラーとして報告しないようにする必要があります。"演算子の注釈" を有効にすると、Embedded Coder は、そのような演算の意図をドキュメント化したコメントを生成されたコード内に挿入します。Polyspace はそうした注釈を使用して、対応する解析結果を非表示にします。注釈は解析のみに使用され、生成された C コードのセマンティクスには影響しません。詳細については、Automated Justification of Coding Rule Violations (Polyspace Bug Finder)を参照してください。

飽和オーバーフローの正当化

このセクションでは、演算子の注釈によって生成されたコード内の飽和動作を正当化する方法を示します。

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

model='mSatAddSub';
open_system(model);

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

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

3. モデルをビルドしてコードを生成します。

evalc('slbuild(''mSatAddSub'')');

生成されたコード ファイルを調べます。

file = fullfile('mSatAddSub_ert_rtw','mSatAddSub.c');
coder.example.extractLines(file,'/* Model step function */',...
    'USub = qY;');

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

コード ジェネレーターは、U1 および U2 に対して最大の組み込み整数型 (32 ビット) を使用して減算を実行します。飽和したすべての結果を直接表すことは不可能なため、生成されたコードでは、まず減算が実行され、次にオーバーフローが検出され、最後に明示的な飽和ロジックが適用されます。Polyspace は、最終的な動作が設計上安全であっても、飽和ロジックを推論しないため、減算に算術オーバーフローのフラグを立てることがあります。

5. [コンフィギュレーション パラメーター] ダイアログ ボックスで [演算子の注釈] を有効にし、モデルをビルドします。

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

6. 生成されたコードを調べます。

file = fullfile('mSatAddSub_ert_rtw','mSatAddSub.c');
coder.example.extractLines(file,'/* Model step function */',...
    'USub = qY;');

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

[演算子の注釈] コンフィギュレーション パラメーターが有効になっている場合、Embedded Coder は /*MW:OvSatOk*/ コメントを挿入します。この注釈は、算術オーバーフローが意図的なものであることを示しており、Polyspace はこの注釈を使用して、コード解析でオーバーフロー エラーを非表示にします。

7. モデルを閉じます。

bdclose(model)

キャリーまたはボローの検出の正当化 (MW:OvCarryOk)

場合によっては、生成されたコードは、キャリー条件またはボロー条件を検出するために、意図的に符号なしラップアラウンド動作を利用します。Polyspace は、ラップアラウンド動作が意図的なものであることを認識しないため、該当する演算に算術オーバーフローのフラグを立てることがあります。

[演算子の注釈] が有効になっている場合、Embedded Coder は MW:OvCarryOk 注釈を挿入して、演算が意図的なものであることを示します。

uint32_T qY;
boolean_T borrow;

qY = U1 - /*MW:OvCarryOk*/ U2;
borrow = (qY > U1);

MW:OvCarryOk 注釈は、オーバーフロー動作が意図的なものであり、キャリー条件またはボロー条件を検出するために使用されていることを示します。Polyspace は、対応するオーバーフロー解析結果を非表示にします。

ビット単位の切り捨ての正当化 (MW:OvBitwiseOk)

まれですが、生成されたコードで、マスキングなどのビット演算によって意図的に上位ビットが破棄されることがあります。Polyspace は、切り捨てが意図的なものであることを認識しないため、そうした算術演算にオーバーフローのフラグを立てることがあります。

[演算子の注釈] が有効になっている場合、Embedded Coder は MW:OvBitwiseOk 注釈を挿入して、この動作を示します。

uint32_T qY;

qY = (U1 + /*MW:OvBitwiseOk*/ U2) & 0xFFU;

MW:OvBitwiseOk 注釈は、その演算によって生じるオーバーフローまたはビット損失が、その後のビット単位の処理のための意図的なものであることを示します。Polyspace は、対応する解析結果を非表示にします。

参考

トピック

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