Main Content

Division by zero

Division by zero occurs

expand all in page

Description

This check determines whether the right operand of a division or modulus operation is zero.

Nonfinite Floats Not Allowed

By default, nonfinite floats are not allowed. A check on a division or modulus operation is:

  • Red, if the right operand is zero on all execution paths through the operation.

  • Orange, if the right operand is zero on some of the execution paths.

  • Green, if the right operand cannot be zero.

Nonfinite Floats Allowed

If you enable a verification mode that incorporates infinities and leave the default that infinities must be allowed, floating point division by zero checks are disabled. In addition, if you specify that the verification must forbid or warn about operations that produce infinities, floating point division by zero errors are shown as overflows. See also Overflow.

To enable this verification mode, use these options:

Examples

expand all

#include <stdio.h>

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

In this example, the denominator x-2 is zero.

Correction — Check for zero denominator

One possible correction is to check for a zero denominator before division.

In a complex code, it is difficult to keep track of values and avoid zero denominators. Therefore, it is good practice to check for zero denominator before every division.

#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));
}

In this example, the denominator x-20 is zero.

Correction — Check for zero denominator

One possible correction is to check for a zero denominator before division.

After several iterations of a for loop, it is difficult to keep track of values and avoid zero denominators. Therefore, it is good practice to check for zero denominator before every division.

#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);
}

In this example, count runs from -100 to 100 through zero. When count is zero, the Division by zero check returns a red error. Because the check returns green in the other for loop runs, the / symbol is orange.

There is also a red Non-terminating loop error on the for loop. This red error indicates a definite error in one of the loop runs.

Correction — Check for zero denominator

One possible correction is to check for a zero denominator before division.

#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);
    }
}

In this example, divisor runs from –1.0 to 1.0 through 0.0. When divisor is 0.0, the Division by zero check returns a red error. Because the check returns green in the other for loop runs, the / symbol is orange.

There is no red Non-terminating loop error on the for loop. The red error does not appear because Polyspace® approximates the values of divisor by a broader range. Therefore, Polyspace cannot determine if there is a definite error in one of the loop runs.

Correction — Check for zero denominator

One possible correction is to check for a zero denominator before division. For float variables, do not check if the denominator is exactly zero. Instead, check whether the denominator is in a narrow range around zero.

#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 ");
    }
}

Check Information

Group: Numerical
Language: C | C++
Acronym: ZDV

See Also

Topics