Exponenta Banner

Субнормальное плавание

Операция с плавающей точкой имеет субнормальные результаты

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

Описание

Эта проверка определяет, приводит ли операция с плавающей точкой к субнормальному результату.

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

По умолчанию результаты проверки не появляются в ваших результатах верификации. Чтобы видеть результаты проверки, измените значение по умолчанию опции Subnormal detection mode (-check-subnormal). Результаты проверки отличаются на основе режима обнаружения, который вы задаете. Во всех режимах кроме allow, чтобы идентифицировать субнормальные результаты, ищут красный или оранжевый Subnormal float, проверяет операции.

РежимПроверяйте цветаПоведение после проверки

forbid:

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

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

Например, если x неизвестен, x * 2 может быть поднормалью, потому что x может быть поднормалью. Результат проверки является оранжевым.

Блокирование проверки.

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

warn-all:

Этот режим подсвечивает все случаи субнормальных значений. Даже если субнормальный результат прибывает из предыдущих субнормальных значений, результат подсвечен.

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

Например, если x неизвестен, x * 2 может быть поднормалью, потому что x может быть поднормалью. Результат проверки является оранжевым.

Неблокирование проверки.

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

warn-first:

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

Цвет проверки зависит от результата операции и значений операнда. Проверка не отмечает субнормальный результат, если она прибывает только из субнормальных операндов.

В этом режиме проверка:

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

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

    Например, если x неизвестен, x * 0.5 может быть поднормалью, даже если x не является поднормалью.

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

    Например, даже если x неизвестен, x * 2 не может быть поднормалью, если x не является поднормалью.

Неблокирование проверки.

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

Если вы принимаете решение проверять на поднормаль, можно также идентифицировать от подсказок, исключает ли переменный диапазон субнормальные значения. Например, если подсказки показывают [-1.0 .. -1.1754E-38] or [-0.0..0.0] or [1.1754E-38..1.0], можно интерпретировать это, переменная не имеет субнормальных значений.

Примеры

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

В следующих примерах DBL_MIN является минимальным нормальным значением, которое может быть представлено с помощью типа double.

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

#include <float.h>

void func(){
    double val = DBL_MIN/4.0;
    double val2 = val * 2.0;
}
В этом примере первая проверка Subnormal float является красной, потому что результатом DBL_MIN/4.0 является поднормаль. Красная проверка останавливает верификацию. Следующая операция, val * 2.0, не проверяется для ошибок времени выполнения.

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

#include <float.h>

void func(){
    double val = DBL_MIN/4.0;
    double val2 = val * 2.0;
}
В этом примере обе проверки Subnormal float являются красными, потому что обе операции имеют субнормальные результаты.

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

#include <float.h>

void func(){
    double val = DBL_MIN/4.0;
    double val2 = val * 2.0;
}
В этом примере DBL_MIN не является поднормалью, но результатом DBL_MIN/4.0 является поднормаль. Первая проверка Subnormal float является красной. Вторая проверка Subnormal float является зеленой. Причина состоит в том, что val * 2.0 является поднормалью только потому, что val является поднормалью. Посредством красных/оранжевых проверок вы видите только первую инстанцию, где субнормальное значение появляется. Вы не видите красные/оранжевые проверки от тех субнормальных значений распространение к последующим операциям.

В следующих примерах arg1 и arg2 неизвестны. Верификация принимает, что они могут принять, все значения допускали тип double.

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

void func (double arg1, double arg2) {
	  double difference1 = arg1 - arg2;
	  double difference2 = arg1 - arg2;
	  double val1 = difference1 * 2;
	  double val2 = difference2 * 2;
}
В этом примере difference1 может быть поднормалью, если arg1 и arg2 достаточно близки. Первая проверка Subnormal float является оранжевой. После этой проверки верификация исключает из фактора следующее:

  • Близкие значения arg1 и arg2, который привел к субнормальному значению difference1.

    В последующей операции arg1 - arg2 проверка Subnormal float является зеленой, и difference2 не является поднормалью. Результат проверки на difference2 * 2 является зеленым по той же причине.

  • Субнормальное значение difference1.

    В последующей операции difference1 * 2 проверка Subnormal float является зеленой.

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

void func (double arg1, double arg2) {
	  double difference1 = arg1 - arg2;
	  double difference2 = arg1 - arg2;
	  double val1 = difference1 * 2;
	  double val2 = difference2 * 2;
}
В этом примере эти четыре операции могут иметь субнормальные результаты. Четыре проверки Subnormal float являются оранжевыми.

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

void func (double arg1, double arg2) {
	  double difference1 = arg1 - arg2;
	  double difference2 = arg1 - arg2;
	  double val1 = difference1 * 2;
	  double val2 = difference2 * 2;
}
В этом примере, если arg1 и arg2 достаточно близки, difference1 и difference2 могут быть поднормалью. Первые две проверки Subnormal float являются оранжевыми. val1 и val2 не могут быть поднормалью, если difference1 и difference2 не являются также поднормалью. Последние две проверки Subnormal float являются зелеными. Посредством красных/оранжевых проверок вы видите только первую инстанцию, где субнормальное значение появляется. Вы не видите красные/оранжевые проверки от тех субнормальных значений распространение к последующим операциям.

void main() {
    float d = 1e-38;	
    float e = 1e-38 - 1e-39; 
}

В этом примере две красных проверки появляются в обоих режимах warn-first и warn-all (режим forbid предотвращает анализ после первой красной проверки).

Литеральные константы, такие как 1e-38 имеют тип данных double. Если вы присваиваете литеральную константу переменной с более узким типом float, постоянная сила не является представимой в этом типе. Эта проблема обозначается с красными проверками. Проверки отмечают преобразование от double до float во время присвоения.

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

Группа: числовой
Язык: C | C++
Акроним: ПОДНОРМАЛЬ

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

| |

Темы

Введенный в R2017b

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