Exponenta Banner

Subnormal float

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

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

Описание

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

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

По умолчанию результаты проверки не появляются в ваших результатах верификации. Чтобы видеть результаты проверки, измените значение по умолчанию опции 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
Поддержка