無限大 (`-check-infinite`)

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

説明

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

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

オプションの設定

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

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

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

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

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

設定

既定値: allow

allow

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

たとえば次のコードでは、[オーバーフロー] チェックが行われません。

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

warn-first

検証では演算に対するチェックが生成されます。このチェックでは、オペランド自体は無限大でない場合に演算の結果が無限大になるかどうかが判定されます。無限大になる実行スレッドは検証で終了されません。

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

たとえば次のコードでは、無限大に対する [オーバーフロー] チェックがブロックされません。

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

/ 演算に対する [オーバーフロー] チェックがレッドになりますが、検証は続行されます。たとえば、return ステートメントの x に対するグリーンの [未初期化ローカル変数] チェックが表示されます。

forbid

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

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

たとえば次のコードでは、無限に対する [オーバーフロー] チェックがブロックされます。

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

/ 演算に対する [オーバーフロー] チェックがレッドになるため、検証が停止します。たとえば、return ステートメントの x に対する [未初期化ローカル変数] チェックは表示されません。

依存関係

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

コマンドライン情報

パラメーター: -check-infinite

値: allow | warn-first | forbid

既定値: allow

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

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

バージョン履歴

R2016a で導入

参考

Polyspace 解析オプション

非有限の浮動小数点を検討 (-allow-non-finite-floats) | NaN (-check-nan)

Polyspace 結果

オーバーフロー

無限大 (-check-infinite)

説明