メインコンテンツ

ゼロ除算

説明

このチェックは、除算またはモジュラス演算の右側オペランドが 0 かどうかを判定します。

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

既定では、非有限の浮動小数点は許可されません。除算またはモジュラス演算に対するチェックは、次のように示されます。

  • 演算でのすべての実行パスで右側オペランドが 0 の場合は、レッド

  • 一部の実行パスで右側オペランドが 0 の場合は、オレンジ

  • 右側オペランドを 0 にできない場合は、グリーン

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

無限大を組み込んだ検証モードを有効にし、無限大を許容する既定の設定のままにした場合は、浮動小数点のゼロ除算チェックが無効にされます。さらに、検証で無限大を生成する演算を禁止するように指定しているか、このような演算に関して警告するように指定している場合、浮動小数点のゼロ除算エラーはオーバーフローとして示されます。オーバーフローも参照してください。

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

すべて展開する

#include <stdio.h>

void main() {
    int x=2;
    printf("Quotient=%d",100/(x-2));
}

この例では、分母 x-2 はゼロです。

修正 — ゼロ分母をチェック

1 つの修正方法として、除算の前のゼロ分母のチェックがあります。

複雑なコードでは、値を追跡してゼロ分母を回避するのは困難です。したがって、すべての除算の前でゼロ分母をチェックすることをお勧めします。

#include <stdio.h>
int input();
void main() {
    int x=input();
    if(x>0) { //Avoid overflow
        if(x!=2 && x>0)
            printf("Quotient=%d",100/(x-2));
        else
            printf("Zero denominator.");
    }
}
#include <stdio.h>
void main() {
    int x=-10;
    for (int i=0; i<10; i++)
        x+=3;
    printf("Quotient=%d",100/(x-20));
}

この例では、分母 x-20 はゼロです。

修正 — ゼロ分母をチェック

1 つの修正方法として、除算の前のゼロ分母のチェックがあります。

for ループが何回か反復した後、値を追跡してゼロ分母を回避するのは困難です。したがって、すべての除算の前でゼロ分母をチェックすることをお勧めします。

#include <stdio.h>
#define MAX 10000
int input();

void main() {
    int x=input();
    for (int i=0; i<10; i++) {
        if(x < MAX) //Avoid overflow
            x+=3;
    }

    if(x>0) { //Avoid overflow
        if(x!=20)
            printf("Quotient=%d",100/(x-20));
        else
            printf("Zero denominator.");
    }
}
#include<stdio.h>

void main() {
    printf("Sequence of ratios: \n");
    for(int count=-100; count<=100; count++)
        printf(" %.2f ", 1/count);
}

この例では、count は -100 から、ゼロを通過して 100 まで実行されます。count がゼロのとき、[ゼロ除算] チェックはレッド エラーを返します。このチェックは他の for ループの実行ではグリーンを返すので、/ 記号はオレンジになります。

また、この for ループには [無限ループ] のレッド エラーもあります。このレッド エラーは、ループ実行の 1 つにおける明確なエラーを示します。

修正 — ゼロ分母をチェック

1 つの修正方法として、除算の前のゼロ分母のチェックがあります。

#include<stdio.h>

void main() {
    printf("Sequence of ratios: \n");
    for(int count=-100; count<=100; count++) {
        if(count != 0)
            printf(" %.2f ", 1/count);
        else
            printf(" Infinite ");
    }
}
#include <stdio.h>
#include <math.h>

#define stepSize 0.1

void main() {
    float divisor = -1.0;
    int numberOfSteps = (int)((2.0*1.0)/stepSize);

    printf("Divisor running from -1.0 to 1.0\n");
    for(int count = 1; count <= numberOfSteps; count++) {
        divisor+= stepSize;
	divisor = ceil(divisor * 10.) / 10.; // one digit of imprecision
        printf(" .2f ", 1.0/divisor);
    }
}

この例では、divisor は -1.0 から、0.0 を通過して 1.0 まで実行されます。divisor が 0.0 のとき、[ゼロ除算] チェックはレッド エラーを返します。このチェックは他の for ループの実行ではグリーンを返すので、/ 記号はオレンジになります。

この for ループには、[無限ループ] のレッド エラーはありません。Polyspace® では divisor の値がより広い範囲によって近似されるため、レッド エラーは表示されません。したがって、ループの実行の 1 つに明確なエラーがあるかどうかは Polyspace では判別できません。

修正 — ゼロ分母をチェック

1 つの修正方法として、除算の前のゼロ分母のチェックがあります。float 変数の場合、分母が正確に 0 であるかどうかをチェックしません。代わりに、分母がゼロ近辺の狭い範囲内にあるかどうかをチェックします。

#include <stdio.h>
#include <math.h>

#define stepSize 0.1

void main() {
    float divisor = -1.0;
    int numberOfSteps = (int)((2*1.0)/stepSize);

    printf("Divisor running from -1.0 to 1.0\n");;
    for(int count = 1; count <= numberOfSteps; count++) {
        divisor += stepSize;
	divisor = ceil(divisor * 10.) / 10.; // one digit of imprecision
        if(divisor < -0.00001 || divisor > 0.00001)
            printf(" .2f ", 1.0/divisor);
        else
            printf(" Infinite ");
    }
}

チェック情報

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