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 mode (режим forbid mode предотвращает анализ после первой красной проверки).

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

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

Группа: Численный
Язык: C | C++
Акроним: SUBNORMAL

См. также

| |

Темы

Введенный в R2016b

Документация Polyspace Code Prover

Поддержка