-check-subnormal)Обнаружьте операции, которые приводят к субнормальным значениям с плавающей точкой
Эта опция влияет на анализ Программы автоматического доказательства Кода только.
Укажите, что верификация должна проверять операции с плавающей точкой на субнормальные результаты.
Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция находится на узле 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 |
Пример (Программа автоматического доказательства Кода): Polyspace Code Prover - источники |
Пример (сервер программы автоматического доказательства кода):
сервер программы автоматического доказательства полипробела кода - источники |