Exponenta Banner

Division by zero

Деление на нуль происходит

расширьте все на странице

Описание

Эта проверка определяет, является ли правильный операнд деления или операции модуля нулем.

Неличные плавания, не позволенные

По умолчанию неличные плавания не позволены. Проверка на делении или операции модуля:

  • Красный, если правильный операнд является нулем на всех путях к выполнению посредством операции.

  • Оранжевый, если правильный операнд является нулем на некоторых путях к выполнению.

  • Зеленый, если правильный операнд не может быть нулем.

Неличные позволенные плавания

Если вы включаете режим верификации, который включает бесконечности, и оставьте значение по умолчанию, которое должны быть позволены бесконечности, деление с плавающей точкой на нулевые проверки отключены. Кроме того, если вы указываете, что верификация должна запретить или предупредить об операциях, которые производят бесконечности, деление с плавающей точкой на нулевые ошибки показываются переполнением. См. также Overflow.

Чтобы включить этот режим верификации, используйте эти опции:

Примеры

развернуть все

#include <stdio.h>

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

В этом примере, знаменатель x-2 нуль.

Коррекция — Проверка на нулевой знаменатель

Одна возможная коррекция должна проверять на нулевой знаменатель перед делением.

В сложном коде это затрудняет, чтобы отслеживать значения и избежать нулевых знаменателей. Поэтому это - хорошая практика, чтобы проверять на нулевой знаменатель перед каждым делением.

#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 нуль.

Коррекция — Проверка на нулевой знаменатель

Одна возможная коррекция должна проверять на нулевой знаменатель перед делением.

После нескольких итераций 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 нуль, проверка Division by zero возвращает красную ошибку. Поскольку проверка возвращается зеленый в другом for запуски цикла, / символ является оранжевым.

На for существует также красная ошибка Non-terminating loop цикл. Эта красная ошибка указывает на определенную ошибку в одном из запусков цикла.

Коррекция — Проверка на нулевой знаменатель

Одна возможная коррекция должна проверять на нулевой знаменатель перед делением.

#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 до 1,0 до 0,0. Когда divisor 0.0, проверка Division by zero возвращает красную ошибку. Поскольку проверка возвращается зеленый в другом for запуски цикла, / символ является оранжевым.

На for нет никакой красной ошибки Non-terminating loop цикл. Красная ошибка не появляется потому что Polyspace® аппроксимирует значения divisor более широкой областью значений. Поэтому Polyspace не может определить, существует ли определенная ошибка в одном из запусков цикла.

Коррекция — Проверка на нулевой знаменатель

Одна возможная коррекция должна проверять на нулевой знаменатель перед делением. Для float переменные, не проверяйте, ниже ли знаменатель нуля. Вместо этого проверяйте, является ли знаменатель в узком диапазоне вокруг нуля.

#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

Смотрите также

Темы

Документация Polyspace Code Prover

Поддержка