NaN (-check-nan)

結果が NaN になる浮動小数点演算の処理方法の指定

説明

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

結果が NaN になる浮動小数点演算を解析でどのように処理しなければならないかを指定します。

オプションの設定

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

  • Polyspace® ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成で [チェック動作] ノードを選択してから、このオプションを選択します。同時に有効にしなければならない他のオプションについては、依存関係を参照してください。

  • Polyspace Platform ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成の [静的解析] タブで [実行時エラー] 、 [チェック動作] ノードを選択してから、このオプションを選択します。同時に有効にしなければならない他のオプションについては、依存関係を参照してください。

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

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

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

解析で非有限の浮動小数点を考慮しなければならないことを指定する場合、既定では、解析はこのような演算にフラグを付けません。このオプションを使用して、非有限の浮動小数点を組み込んだ状態を維持したまま、このような演算を検出します。

設定

既定値: allow

allow

検証では演算に対するチェックが生成されません。

たとえば次のコードでは、[浮動小数点での無効な演算] チェックが行われません。

double func(void) {
    double x=1.0/0.0;
    double y=x-x;
    return y;
}
warn-first

検証では演算に対するチェックが生成されます。このチェックでは、オペランド自体は NaN でない場合に演算の結果が NaN になるかどうかが判定されます。たとえば、このチェックでは、val1 と val2 が "両方" NaN でないときに結果が NaN になる可能性がある場合にのみ、演算 val1 + val2 にフラグが付けられます。NaN になる実行スレッドは検証で終了されません。

すべての実行パスで結果が必ず NaN になる演算が検証で検出され、オペランド自体は NaN でない場合、チェックはレッドになります。演算が NaN になる可能性がある場合は、チェックはオレンジになります。

たとえば次のコードでは、NaN に対する [浮動小数点での無効な演算] チェックがブロックされません。

double func(void) {
    double x=1.0/0.0;
    double y=x-x;
    return y;
}

- 演算に対する [浮動小数点での無効な演算] チェックがレッドになりますが、検証は続行されます。たとえば、return ステートメントの y に対するグリーンの [未初期化ローカル変数] チェックが表示されます。

forbid

検証で演算に対するチェックが生成され、NaN になる実行スレッドが終了されます。

チェックがレッドの場合、そのチェックと同じスコープにある残りのコードについては検証は続行されません。チェックがオレンジの場合、検証は続行されますが、NaN になった変数値は対象から除外されます。

たとえば次のコードでは、NaN に対する [浮動小数点での無効な演算] チェックがブロックされます。

double func(void) {
    double x=1.0/0.0;
    double y=x-x;
    return y;
}

- 演算に対する [浮動小数点での無効な演算] チェックがレッドになるため、検証が停止します。たとえば、return ステートメントの y に対する [未初期化ローカル変数] チェックは表示されません。

また、/ 演算に対する NaN についての [浮動小数点での無効な演算] チェックもグリーンで表示されます。

依存関係

このオプションを使用するには、無限大と NaN を組み込んだ検証モードを有効にしなければなりません。詳細は、非有限の浮動小数点を検討 (-allow-non-finite-floats) を参照してください。

コマンド ライン情報

パラメーター: -check-nan
値: allow | warn-first | forbid
既定値: allow
例 (Code Prover): polyspace-code-prover -sources file_name -check-nan forbid
例 (Code Prover Server): polyspace-code-prover-server -sources file_name -check-nan forbid

バージョン履歴

R2016a で導入

参考

Polyspace 解析オプション

Polyspace 結果

トピック