Exponenta Banner

Invalid operation on floats

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

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

Описание

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

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

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

  • Orange, если операция создает 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

Поддержка