非正規検出モード (-check-subnormal)

非正規浮動小数点値になる演算の検出

説明

このオプションは Code Prover 解析のみに影響します。

結果が非正規になる浮動小数点演算が、検証でチェックされなければならないことを指定します。

オプションの設定

以下のいずれかの方法を使用してオプションを設定します。

• Polyspace^® ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成で [チェック動作] ノードを選択してから、このオプションを選択します。

• Polyspace Platform ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成の [静的解析] タブで [実行時エラー] 、 [チェック動作] ノードを選択してから、このオプションを選択します。

• コマンド ラインとオプション ファイル: オプション -check-subnormal を使用します。コマンド ライン情報を参照してください。

このオプションを使用する理由

このオプションを使用して、結果が非正規値になる浮動小数点演算を検出します。

非正規数とは、仮数部の上位桁に 0 を付けずに表現できる最小の浮動小数点数よりも小さな値のことです。非正規数の存在は有効桁数が失われることを示します。この損失はそれ以降の演算に累積し、最終的には予期しない値につながります。非正規数は、ハードウェアのサポートがないターゲットでの実行速度を低下させる可能性もあります。

設定

既定値: allow

allow

検証では、結果が非正規になる演算がチェックされません。

forbid

検証では、結果が非正規になる演算がチェックされます。

検証では、結果が非正規になる実行パスが停止され、非正規値がそれ以上伝播しなくなります。したがって、実際には、最初に出現した非正規数のみが表示されます。

warn-all

検証では、結果が非正規になる演算がチェックされ、非正規値の出現箇所がすべて強調表示されます。結果が非正規となった原因がそれ以前の非正規値にある場合でも、その結果が強調表示されます。

チェックがレッドになっても、検証が続行されます。

warn-first

検証では、結果が非正規になる演算がチェックされますが、非正規値の最初の出現箇所のみが強調表示されます。非正規値がそれ以降の演算結果に非正規値を伝播させている場合、このような後続の結果は強調表示されません。

チェックがレッドになっても、検証が続行されます。

各モードの結果の色についての詳細は、非正規浮動小数点を参照してください。

ヒント

• 非正規値ではないオペランドから非正規の結果になる演算のみを表示する場合は、warn-first モードを使用します。

  たとえば、次のコードの arg1 と arg2 は不明です。検証では、これらが double 型で許容されるすべての値を取り得ると仮定されます。この仮定により、特定の演算の結果が非正規になる可能性があります。warn-first モードを使用すると、結果が非正規になる最初の演算が強調表示されます。

  warn-all

  warn-first

  void func (double arg1, double arg2) { double difference1 = arg1 - arg2; double difference2 = arg1 - arg2; double val1 = difference1 * 2; double val2 = difference2 * 2; } この例では、4 つすべての演算の結果が非正規になる可能性があります。結果が非正規になる演算のチェックでは、この 4 つがオレンジになります。

  void func (double arg1, double arg2) { double difference1 = arg1 - arg2; double difference2 = arg1 - arg2; double val1 = difference1 * 2; double val2 = difference2 * 2; } この例では、arg1 と arg2 がきわめて近い値の場合、difference1 と difference2 は非正規になる可能性があります。非正規結果のチェックでは、最初の 2 つがオレンジになります。difference1 と difference2 の結果が非正規にならない限り、val1 と val2 が非正規になる可能性はありません。非正規結果のチェックでは、最後の 2 つはグリーンです。 レッド/オレンジ チェックでは、非正規値になる最初の出現箇所のみが表示されます。これらの非正規値がそれ以降の演算に伝播してもレッド/オレンジ チェックは表示されません。

• 非正規値の原因になった演算を表示し、同じ原因で結果が非正規になる演算を 2 回目以降表示しない場合は、forbid モードを使用します。

  たとえば、次のコードの arg1 と arg2 は不明です。検証では、これらが double 型で許容されるすべての値を取り得ると仮定されます。この仮定により、arg1-arg2 の結果が非正規になる可能性があります。forbid モードを使用し、演算 arg1-arg2 が 2 回続けて実行される場合、最初の演算のみが強調表示されます。2 回目の演算の結果が非正規になるのは、最初の演算と原因が同じであるため、2 回目の演算は強調表示されません。

  warn-all

  forbid

  void func (double arg1, double arg2) { double difference1 = arg1 - arg2; double difference2 = arg1 - arg2; double val1 = difference1 * 2; double val2 = difference2 * 2; } この例では、4 つすべての演算の結果が非正規になる可能性があります。結果が非正規になる演算のチェックでは、この 4 つがオレンジになります。

  void func (double arg1, double arg2) { double difference1 = arg1 - arg2; double difference2 = arg1 - arg2; double val1 = difference1 * 2; double val2 = difference2 * 2; } この例では、arg1 と arg2 がきわめて近い値の場合、difference1 は非正規になる可能性があります。非正規結果のチェックでは、最初の演算がオレンジになります。このチェックの後の検証では、以下が検討対象から除外されます。 arg1 と arg2 が近い値で、それが原因で difference1 の結果が非正規値になる場合。 それ以降の演算 arg1 - arg2 のチェックはグリーンになり、difference2 の結果は非正規になりません。difference2 * 2 のチェック結果は、同じ理由でグリーンになります。 difference1 が非正規値の場合。 それ以降の演算 difference1 * 2 のチェックはグリーンになります。

コマンド ライン情報

パラメーター: -check-subnormal

値: allow | warn-first | warn-all | forbid

既定値: allow

例 (Code Prover): polyspace-code-prover -sources file_name -check-subnormal forbid

例 (Code Prover Server): polyspace-code-prover-server -sources file_name -check-subnormal forbid

バージョン履歴

R2016b で導入

参考

Polyspace 結果

• 非正規浮動小数点

トピック

• Polyspace 解析オプションの指定
• Code Prover の実行時チェックの変更または無効化