オーバーフロー

算術演算が原因のオーバーフロー

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

説明

算術演算に関するこのチェックでは、結果がオーバーフローするかどうかを判別します。このチェックの結果は、無限大や NaN などの非有限の浮動小数点の結果を許可しているかどうかによって異なります。

チェックの結果は、指定した浮動小数点の丸めモードにも依存します。既定では、丸めモードは to-nearest です。浮動小数点の丸めモード (-float-rounding-mode) を参照してください。

非有限の浮動小数点を許可しない

既定では、非有限の浮動小数点は許可されません。演算の結果が許可された範囲から外れると、オーバーフローが発生します。チェックは次のようになります。

  • 演算の結果が許可された範囲から外れる場合はレッド。

  • 一部の実行パスで演算の結果が許可された範囲から外れる場合はオレンジ。

  • 演算の結果が許可された範囲から外れない場合はグリーン。

オーバーフロー チェックの動作を微調整するには、以下のオプションを使用し、引数 [forbid]、[allow]、または [warn-with-wrap-around] を指定します。

算術演算で許可される範囲はオペランドのデータ型で決まります。演算にオペランドが 2 つある場合、検証では ANSI® C の変換ルールを使用して共通のデータ型を判別します。この共通のデータ型により、許可される範囲が決まります。

変換ルールのいくつかの例については、暗黙的なデータ型の変換に関する Code Prover の仮定を参照してください。

非有限の浮動小数点を許可する

無限大を組み込んだ検証モードを有効にし、無限大になる演算について検証で警告するように指定している場合、チェックは次のようになります。

  • ソフトウェアで考慮されるすべての実行パスで演算が無限大になり、オペランド自体が無限大でない場合はレッド。

  • オペランド自体が無限大でないときに一部の実行パスで演算が無限大になる場合はオレンジ。

  • オペランド自体が無限大でなければ演算が無限大にならない場合はグリーン。

検証で無限大になる演算を禁止するように指定している場合、チェックの色は演算の結果にのみ依存します。色はオペランドには依存しません。

この検証モードを有効にするには、以下のオプションを使用します。

例

すべて展開する

void main() {
  int i=1;
  i = i << 30; //i = 2^30
  i = 2*i-2;
}

この例では、演算 2*i の結果、231 の値が得られます。int 型が 32 ビットのターゲットで保有できる最大値は 231-1 であるため、乗算に対する [オーバーフロー] チェックはレッド エラーを生成します。

void main(void)
 {
   int i;
   int shiftAmount = 1;

   i = 1090654225 << shiftAmount; 
 }

この例では、符号付き整数で左シフトが実行されたため、[オーバーフロー] エラーが発生します。

#include <float.h>

void main() {
 float val = FLT_MAX;
 val = val * 2 + 1.0;
}

この例で FLT_MAX は、32 ビットのターゲットにおいて float で表せる最大値です。このため、演算 val * 2 の結果は [オーバーフロー] エラーになります。

void func(void) {
   float fVal = -2.0f;
   unsigned int iVal = (unsigned int)fVal; 
}

この例では、float から unsigned int へのキャストの [オーバーフロー] チェックが、レッドで表示されます。C99 規格 (段落 6.3.1.4 に対する脚注) によると、コードを移植可能に保ちながら浮動小数点値から符号なし整数に変換できる値の範囲は (-1, MAX + 1) です。この範囲外の浮動小数点値から符号なし整数への変換は、明確に定義されていません。ここで、MAX は、符号なし整数型に格納できる最大数です。

ターゲットでコードを実行するときにランタイム エラーが発生しない場合でも、別のターゲットではキャストに失敗する可能性があります。

修正 — 最初に符号付き整数にキャスト

1 つの解決策として、浮動小数点値を最初に符号付き整数にキャストします。その後、符号付き整数を符号なし整数型にキャストできます。このようなキャストの場合、変換ルールが明確に定義されています。

void func(void) {
   float fVal = -2.0f;
   int iValTemp = (int)fVal;
   unsigned int iVal = (unsigned int)iValTemp; 
}
#define FLT_MAX 3.40282347e+38F

void float_negative_overflow() {
   float min_float = -FLT_MAX;
   min_float = -min_float * min_float;
}

float_negative_overflow の min_float には、float 型で表すことのできる最小の負の数値が入っています。演算 -min_float * min_float はこの数値よりも小さい負の数値を生成するため、float 型で表すことはできません。[オーバーフロー] チェックはレッド エラーを生成します。

#include <stdio.h>

struct
{
  unsigned int dayOfWeek : 2;
} Week;

void main()
{
  unsigned int two = 2, three = 3, four = 4;
  Week.dayOfWeek = two;
  Week.dayOfWeek = three;
  Week.dayOfWeek = four;
}

この例では、dayOfWeek は 2 ビットを有します。これは符号なし整数であるため、[0,3] の値になる可能性があります。値 4 を dayOfWeek に代入すると、[オーバーフロー] チェックはレッドになります。

符号付き整数および符号なし整数でオーバーフローを検出するには、[構成] ペインの [チェック動作] で、[符号付き整数のオーバーフロー モード] と [符号なし整数のオーバーフロー モード] に [forbid] または [warn-with-wrap-around] を選択します。

forbid モードでの結果:

double func(void) {
    double x=1.0/0.0;
    return x;
}
この例では、/ 演算のどちらのオペランドも無限大ではありませんが、結果が無限大になります。- 演算に対する [オーバーフロー] チェックはレッドになります。forbid モードでは、レッド チェックの後、検証は停止されます。たとえば、return ステートメントの x に対する [未初期化ローカル変数] チェックは表示されません。オプション [非有限の浮動小数点を許可] をオンにしない場合は、無限大が許可されないため [ゼロ除算] チェックが表示されます。

warn-first モードでの結果:

double func(void) {
    double x=1.0/0.0;
    return x;
}
この例では、/ 演算のどちらのオペランドも無限大ではありませんが、結果が無限大になります。- 演算に対する [オーバーフロー] チェックはレッドになります。warn-first モードでのレッド チェックは、他のチェック タイプのレッド チェックとは異なります。レッド チェックの後、検証が停止されません。たとえば、return ステートメントの x に対するグリーンの [未初期化ローカル変数] チェックが表示されます。検証結果の x にカーソルを置くと、値が Inf になっていることがわかります。

forbid モードでの結果:

void func(double arg1, double arg2) {
    double ratio1=arg1/arg2;
    double ratio2=arg1/arg2;
}
この例では、arg1 と arg2 の値を検証で特定できません。検証では、arg1 と arg2 が double のすべての値を取る可能性があると仮定されます。たとえば、arg1 が非ゼロで arg2 がゼロになれば、ratio1=arg1/arg2 の結果が無限大になる可能性があります。したがって、この除算演算に対してオレンジの [オーバーフロー] チェックが表示されます。チェックの後、検証では結果が無限大になる実行スレッドが終了されます。検証では、このオレンジ チェックの後は arg2 がゼロにならないと仮定されます。2 番目の除算演算 ratio2=arg1/arg2 に対する [オーバーフロー] チェックはグリーンになります。

warn-first モードでの結果:

void func(double arg1, double arg2) {
    double ratio1=arg1/arg2;
    double ratio2=arg1/arg2;
}
この例では、arg1 と arg2 の値を検証で特定できません。検証では、arg1 と arg2 が double のすべての値を取る可能性があると仮定されます。たとえば、arg1 が非ゼロで arg2 がゼロになれば、ratio1=arg1/arg2 の結果が無限大になる可能性があります。この除算演算に対してオレンジの [オーバーフロー] チェックが表示されます。warn-first モードでのオレンジ チェックは、他のチェック タイプのオレンジ チェックとは異なります。チェックの後、検証では結果が無限大になる実行スレッドが終了されません。検証では、このオレンジ チェックの後も arg2 の値がゼロであると見なされます。したがって、2 番目の除算演算 ratio2=arg1/arg2 に対する [オーバーフロー] チェックもオレンジになります。

チェック情報

グループ: 数値
言語: C | C++
頭字語: OVFL

参考

| | | | | |

トピック