Exponenta Banner

Недопустимая операция на плаваниях

Результатом операции с плавающей точкой является NaN для операндов non-NaN

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

Описание

Эта проверка определяет, является ли результатом операции с плавающей точкой NaN. Проверка выполнена, только если вы включаете режим верификации, который включает NaNs, и укажите, что верификация должна подсветить операции тот результат в NaN.

Если вы указываете, что верификация должна произвести предупреждение для NaN, проверка:

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

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

  • Зеленый, если операция не производит NaN, если операндами не является NaN.

Если вы указываете, что верификация должна запретить NaN, цвет проверки зависит от результата операции только. Цвет не зависит от операндов.

Проверка также подсвечивает преобразования от переменных с плавающей точкой до целых чисел, где переменной с плавающей точкой может быть NaN. В этом случае проверка всегда выполняется, когда вы включаете NaNs в верификацию, и не разрешает NaNs, как введено преобразованию.

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

Примеры

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

Результаты в режиме forbid:

double func(void) {
    double x=1.0/0.0;
    double y=x-x;
    return y;
}
В этом примере оба операндами операции - не является NaN, но результатом является NaN. Invalid operation on floats начинает работу, операция - является красной. В режиме forbid, остановки верификации после красной проверки. Например, проверка Non-initialized local variable не появляется на y в операторе return.

Результаты в режиме warn-first:

double func(void) {
    double x=1.0/0.0;
    double y=x-x;
    return y;
}
В этом примере оба операндами операции - не является NaN, но результатом является NaN. Invalid operation on floats начинает работу, операция - является красной. Красные регистрации режима warn-first отличаются от красных проверок на другие типы проверки. Верификация не останавливается после красной проверки. Например, зеленая проверка Non-initialized local variable появляется на y в операторе return. Если вы устанавливаете свой курсор на y в результате верификации, вы видите, что это имеет значение NaN.

Результаты в режиме forbid:

double func(double arg1, double arg2) {
    double ret=arg1-arg2;
    return ret;
}
В этом примере значения arg1 и arg2 неизвестны верификации. Верификация принимает, что arg1 и arg2 могут быть и бесконечными, например, и результатом arg1-arg2 может быть NaN. В режиме forbid, после проверки, верификация отключает путь к выполнению, который приводит к NaN. Если вы устанавливаете свой курсор на ret в операторе return, это не имеет значения NaN.

Результаты в режиме warn-first:

double func(double arg1, double arg2) {
    double ret=arg1-arg2;
    return ret;
}
В этом примере значения arg1 и arg2 неизвестны верификации. Верификация принимает, что arg1 и arg2 могут быть и бесконечными, например, и результатом arg1-arg2 может быть NaN. Оранжевые регистрации режима warn-first отличаются от оранжевых проверок на другие типы проверки. После проверки верификация не отключает путь к выполнению, который приводит к NaN. Если вы устанавливаете свой курсор на ret в операторе return, это продолжает иметь значение NaN наряду с другими возможными значениями.

double func(double arg1, double arg2) {
    double z=arg1-arg2;
    return z;
}

void caller() {
    double x=1.0/0.0;
    double y=x-x;
    func(x,x);
    func(y,y);
}

В этом примере, в func, результатом операции - всегда является NaN, но проверка Invalid operation on floats является оранжевой вместо красного.

  • В первом вызове func и операнды arg1 и arg2 не является NaN, но результатом является NaN. Так, проверка является красной.

  • Во втором вызове func и операнды arg1 и arg2 является NaN, и поэтому результатом является NaN. Так, проверка является зеленой, указывая, что результатом не является NaN, если операндами не является NaN.

Комбинируя цвета для двух вызовов func, проверка является оранжевой.

В примере опция использовался -check-nan warn-first.

void func() {
    double x= 1.0/0.0;
    double y= x-x;
    int z = y;
}

В этом примере проверка Invalid operation on floats обнаруживает присвоение NaN к целочисленной переменной z.

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

Информация о результате

Группа: числовой
Язык: C | C++
Акроним: INVALID_FLOAT_OP

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

| |

Темы

Введенный в R2016a

Документация Polyspace Code Prover
Поддержка