浮動小数点のオーバーフロー

浮動小数点間の演算によるオーバーフロー

このページをすべて展開する

説明

この欠陥は、浮動小数点変数に対する演算が、その演算が使用するデータ型では表せない値になる場合に発生します。このデータ型はオペランドの型に応じて異なります。このデータ型によって、結果を格納するために割り当てられるバイト数が決まり、許容される値の範囲が制限されます。

次の点に注意してください。

  • オーバーフローの判別に使用されるデータ型は、オペランドのデータ型に基づいています。演算結果を別の変数に割り当てると、別のチェッカー [浮動小数点変換のオーバーフロー] が、その割り当てられた値によっても割り当て先の変数がオーバーフローするかどうかを判別します。たとえば次のような演算があるとします。

    res = x + y;
    このチェッカーは res の型ではなく x および y の型に基づいて、オーバーフローをチェックします。浮動小数点変換のオーバーフローのチェッカーは、res の型に基づいてオーバーフローをチェックします。

  • 二項演算の 2 つのオペランドで、演算発生前にプロモーションが行われることがあります。暗黙的なデータ型の変換に関する Code Prover の仮定 (Polyspace Code Prover)も参照してください。

異なる型への正確なストレージ割り当てはプロセッサに依存します。ターゲット プロセッサ タイプ (-target)を参照してください。

リスク

オーバーフローにより、計算の結果が予期しない値になる場合があります。実装に使用している丸めモードに応じて、結果が無限大または最大の有限値になる可能性があります。以降の計算でオーバーフローの発生した計算の結果を使用しており、オーバーフローを考慮していない場合、予期しない結果になることがあります。

修正方法

修正方法は欠陥の根本原因によって異なります。多くの場合、結果の詳細 (または Polyspace as You Code のソース コード ツールヒント) には欠陥につながる一連のイベントが表示されます。そのシーケンス内のどのイベントについても修正を実装できます。結果の詳細にイベント履歴が表示されない場合は、ソース コード内で右クリック オプションを使用して、欠陥に関連する変数のこれまでの参照を検索し、関連するイベントを検出できます。Polyspace デスクトップ ユーザー インターフェイスでの Bug Finder の結果の解釈またはPolyspace Access Web インターフェイスでの Bug Finder の結果の解釈 (Polyspace Access)も参照してください。

以下の修正例を参照してください。

問題を修正しない場合は、改めてレビューされないように結果またはコードにコメントを追加します。詳細は、以下を参照してください。

既定では、Bug Finder 解析は無限大と NaNs を認識しません。結果が無限大および NaNs になる演算には、欠陥としてフラグが設定される可能性があります。コードで無限大および NaN の値を処理するには、オプション [非有限の浮動小数点を検討] (-allow-non-finite-floats) を使用します。

チェッカーの拡張

入力値が不明であり、入力のサブセットのみがエラーの原因となっている場合、既定の Bug Finder 解析ではこの欠陥が報告されない可能性があります。特定のシステム入力値を原因とする欠陥の有無をチェックするには、より厳密な Bug Finder 解析を実行してください。特定のシステム入力値から欠陥を見つけるための Bug Finder チェッカーの拡張を参照してください。

例

すべて展開する

#include <float.h>

float square(void) {

   float val = FLT_MAX;
   return val * val;  
}

return ステートメントで、変数 val にそれ自身を乗算しています。val の値は浮動小数点の最大値であり、浮動小数点の最大値の 2 乗は浮動小数点 (この関数の戻り値の型) では表現できません。

修正 — 異なるストレージ型

1 つの修正方法として、演算の結果をより大きいデータ型に保存することができます。この例では、float ではなく double を返すことでオーバーフローの欠陥を修正できます。

#include <float.h>

double square(void) {
    float val = FLT_MAX;

    return (double)val * (double)val;  
}

結果情報

グループ: 数値
言語: C | C++
既定値: オフ
コマンド ライン構文: FLOAT_OVFL
影響度: Low

バージョン履歴

R2013b で導入

参考

| |

トピック