このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。

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

無限大と NaN を組み込んだ解析モードの有効化

説明

浮動小数点演算に対して、無限大と NaN を組み込んだ解析モードを有効にします。

オプションの設定

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

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

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

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

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

Code Prover

既定では、解析に無限大と NaN は組み込まれていません。たとえば、ゼロ除算が発生し結果が無限大になる可能性を考慮しない実行スレッドは、解析によって終了されます。

isinf または isnan などの関数を使用してコードで無限大と NaN を考慮する場合は、このオプションを設定します。このオプションを設定し、たとえば、ゼロ除算が発生すると、実行スレッドはこの除算結果を無限大として続行します。

コードで無限大と NaN を考慮していることが確実な場合は、このオプションを単独で設定します。このオプションを単独で使用すると、浮動小数点演算の数値チェックの多くが事実上に無効になります。ほとんどの場合無限大と NaN を考慮しているとしても、すべての状況で考慮されるかどうかが不明瞭な場合は、以下の追加オプションを設定します。

Bug Finder

解析で、isinf または isnan を使用した比較にデッド コードのフラグが設定される場合、このオプションを使用します。既定では、Bug Finder 解析に無限大と NaN は組み込まれていません。

設定

オン

解析で無限大と NaN が許容されます。このモードでは、たとえば次のようになります。

  • 解析では、浮動小数点演算の結果が無限大や NaN になる可能性があると想定されます。

    オプション [無限大] (-check-infinite) および [NaN] (-check-nan) を使用して、結果が非有限になる演算を強調表示したり、結果が非有限になった時点で実行スレッドを停止したりできます。これらのオプションは、Bug Finder 解析には使用できません。

  • 解析では、値が不明な浮動小数点変数について、無限大と NaN を含む、その型に許容される任意の値を取る可能性があると想定されます。値が不明な浮動小数点変数には、スタブ関数の volatile 変数や戻り値が含まれます。

オフ (既定の設定)

解析で無限大と NaN が許容されません。このモードでは、たとえば次のようになります。

  • Code Prover 解析では、すべての実行パスで結果が必ず無限大または NaN になる浮動小数点演算に対してはレッド チェックが生成されます。結果が無限大または NaN になる可能性がある浮動小数点演算に対してはオレンジ チェックが生成されます。

  • Code Prover 解析では、値が不明な浮動小数点変数について、全範囲のうちの有限の値になると想定されます。

  • Bug Finder 解析では、isinf を使用した無限大を含む比較がデッド コードとして示されます。

ヒント

  • IEEE® 754 規格では、コードを中止せずに特定の数値の例外を処理できるように、無限大や NaN などの特殊な量が許可されています。C 標準では、一部の実装で無限大と NaN がサポートされています。

    • コンパイラで無限大と NaN がサポートされており、それらをコードで明示的に考慮する場合は、このオプションを使用して検証でも許容されるようにします。

      たとえば、除算の結果が無限大になる場合のアクションとして、コードで別のアクションを指定しているとします。この場合、結果が無限大になる除算演算を検証で強調表示する必要はありません。

    • コンパイラで無限大と NaN がサポートされており、それらをコードで明示的に考慮するかどうかわからない場合は、このオプションを使用して無限大と NaN を検証に組み込むようにします。オプション -check-nan および -check-infinite で引数 warn を使用すると、結果が無限大および NaN になる演算を検証で強調表示し、実行スレッドは中止しないように設定できます。これらのオプションは、Bug Finder 解析には使用できません。

  • Code Prover 解析を実行して、このオプションを使用する場合、オーバーフロー、ゼロ除算、およびその他の数値的なランタイム エラーのチェッカーが無効になります。数値チェックを参照してください。

    Bug Finder 解析を実行して、このオプションを使用すると、次のようになります。

  • このオプションを選択すると、コード内の Code Prover チェックの数やタイプが変更される場合があります。

    たとえば、以下の例では、オプションを選択すると、結果でレッド チェックが 1 つ減り、グリーン チェックが 3 つ増えます。

    無限大と NaN を許容しない無限大と NaN を許容する

    Code Prover で [ゼロ除算] エラーが生成され、検証が停止します。

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

    このオプションを選択した場合、Code Prover で [ゼロ除算] エラーがチェックされません。 

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

    解析では、ゼロ除算が次のような結果になると想定されます。

    • x の値が Inf になる

    • y の値が 0.0 になる

    • z の値が NaN になる

    Polyspace ユーザー インターフェイスで解析結果の y および z にカーソルを置くと、ツールヒントに非有限値 Inf および NaN がそれぞれ表示されます。

コマンド ライン情報

パラメーター: -allow-non-finite-floats
既定値: オフ
例 (Bug Finder): polyspace-bug-finder -sources file_name -allow-non-finite-floats
例 (Code Prover): polyspace-code-prover -sources file_name -allow-non-finite-floats
例 (Bug Finder Server): polyspace-bug-finder-server -sources file_name -allow-non-finite-floats
例 (Code Prover Server): polyspace-code-prover-server -sources file_name -allow-non-finite-floats

バージョン履歴

R2016a で導入

参考

| | |

トピック