-check-subnormal)Обнаружение операций, которые приводят к субнормальным значениям с плавающей точкой
Эта опция влияет только на анализ Code Prover.
Укажите, что верификация должна проверять операции с плавающей точкой на субнормальные результаты.
Пользовательский интерфейс (только для настольных продуктов): В строении проекта опция находится на узле Check Behavior.
Командная строка и файл опций: Используйте опцию -check-subnormal. См. «Информация о командной строке».
Используйте эту опцию, чтобы обнаружить операции с плавающей точкой, которые приводят к субнормальным значениям.
Субнормальные числа имеют величины меньше, чем наименьшее число с плавающей запятой, которое может быть представлено без ведущих нулей в значении и. Наличие субнормальных чисел указывает на потерю значащих цифр. Эта потеря может накопиться за последующие операции и в конечном счете привести к неожиданным значениям. Субнормальные числа могут также замедлить выполнение на целевых устройствах без аппаратной поддержки.
По умолчанию: allow
allow Эта верификация не проверяет операции на субнормальные результаты.
forbid Эта верификация проверяет субнормальные результаты.
Эта верификация останавливает путь выполнения с субнормальным результатом и препятствует дальнейшему распространению субнормальных значений. Поэтому на практике вы видите только первое вхождение субнормального значения.
warn-all Эта верификация проверяет субнормальные результаты и подсветки все вхождения субнормальных значений. Даже если субнормальный результат исходит из предыдущих субнормальных значений, результат подсвечивается.
Проверка продолжается верификация даже если она красная.
warn-first Эта верификация проверяет субнормальные результаты, но только подсвечивает первые вхождения субнормальных значений. Если субнормальное значение переходит к дальнейшим субнормальным результатам, эти последующие результаты не подсвечиваются.
Проверка продолжается верификация даже если она красная.
Для получения дополнительной информации о цветах результатов в каждом режиме смотрите Subnormal float.
Если вы хотите увидеть только те операции, где субнормальное значение происходит из неподнормальных операндов, используйте warn-first режим.
Например, в следующем коде arg1 и arg2 неизвестны. Эта верификация предполагает, что они могут принимать все значения, разрешенные для типа double. Это предположение может привести к субнормальным результатам от определенных операций. Если вы используете warn-first режим, первая операция, вызывающая субнормальный результат, подсвечивается.
warn-all | warn-first |
|---|---|
void func (double arg1, double arg2)
{
double difference1 = arg1 - arg2;
double difference2 = arg1 - arg2;
double val1 = difference1 * 2;
double val2 = difference2 * 2;
}
В этом примере все четыре операции могут иметь субнормальные результаты. Четыре проверки на субнормальные результаты являются оранжевыми. | void func (double arg1, double arg2)
{
double difference1 = arg1 - arg2;
double difference2 = arg1 - arg2;
double val1 = difference1 * 2;
double val2 = difference2 * 2;
}
В этом примере С помощью проверок красного/оранжевого цвета вы видите только первый образец, где появляется субнормальное значение. Вы не видите проверки красного/оранжевого цвета из этих субнормальных значений, распространяющихся на последующие операции. |
Если вы хотите увидеть, где возникает субнормальное значение, и не хотите видеть субнормальные результаты, возникающие из-за одной и той же причины более одного раза, используйте forbid режим.
Например, в следующем коде arg1 и arg2 неизвестны. Эта верификация предполагает, что они могут принимать все значения, разрешенные для типа double. Это предположение может привести к субнормальным результатам для arg1-arg2. Если вы используете forbid и выполните операцию arg1-arg2 дважды последовательно подсвечивается только первая операция. Вторая операция не подсвечивается, потому что субнормальный результат для второй операции возникает из той же причины, что и первая операция.
warn-all | forbid |
|---|---|
void func (double arg1, double arg2)
{
double difference1 = arg1 - arg2;
double difference2 = arg1 - arg2;
double val1 = difference1 * 2;
double val2 = difference2 * 2;
}
В этом примере все четыре операции могут иметь субнормальные результаты. Четыре проверки на субнормальные результаты являются оранжевыми. | void func (double arg1, double arg2)
{
double difference1 = arg1 - arg2;
double difference2 = arg1 - arg2;
double val1 = difference1 * 2;
double val2 = difference2 * 2;
}
В этом примере
|
Параметр: -check-subnormal |
Значение: allow | warn-first | warn-all | forbid |
По умолчанию: allow |
Пример (Code Prover): Polyspace Code Prover -sources |
Пример (Code Prover Server):
polyspace кода -prover-server -sources |