Exponenta Banner
exponenta event banner

Субнормальный поплавок

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

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

Описание

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

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

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

СпособПроверить цветаПоведение после проверки

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;
}
В этом примере первая проверка поднормального плавания имеет красный цвет, поскольку результат 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;
}
В этом примере обе проверки поднормального плавающего положения имеют красный цвет, поскольку обе операции имеют поднормальные результаты.

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

#include <float.h>

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

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

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

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

    В последующей операции difference1 * 2, проверка поднормального поплавка зеленого цвета.

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

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

Результаты в 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 может быть субнормальным. Первые две субнормальные плавающие проверки оранжевые. val1 и val2 не может быть субнормальным, если difference1 и difference2 также являются субнормальными. Последние две субнормальные плавающие проверки имеют зеленый цвет. При проверке красным/оранжевым цветом отображается только первый экземпляр, в котором отображается субнормальное значение. Проверки красного/оранжевого цвета из этих субнормальных значений, распространяющихся на последующие операции, не отображаются.

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++
Аббревиатура: SUBNORMAL

См. также

| |

Темы

Представлен в R2016b

Документация по программе проверки кода Polyspace

Поддержка