-allow-non-finite-floats)Включите режим анализа, который включает бесконечности и NaNs
Включите режим анализа, который включает бесконечности и NaNs для операций с плавающей точкой.
Пользовательский интерфейс (только для настольных продуктов): В строении проекта опция находится на узле Check Behavior.
Командная строка и файл опций: Используйте опцию -allow-non-finite-floats. См. «Информация о командной строке».
По умолчанию анализ не включает бесконечности и NaNs. Для образца анализ завершает поток выполнения, где происходит деление по нулю, и не считает, что результат может быть бесконечным.
Если вы используете такие функции, как isinf или isnan и учитывайте бесконечности и NaNs в вашем коде, установите эту опцию. Когда вы устанавливаете эту опцию, и для образца происходит деление по нулю, поток выполнения продолжается с бесконечностью в результате деления.
Установите эту опцию в одиночку, если вы уверены, что в вашем коде учтены бесконечности и NaNs. Использование одной только опции эффективно отключает многие числовые проверки на операциях с плавающей точкой. Если вы обычно учитывали бесконечности и NaNs, но не уверены, что рассмотрели все ситуации, установите эти дополнительные опции:
Infinities (-check-infinite): Использовать warn-first.
NaNs (-check-nan): Использовать warn-first.
Если анализ помечает сравнения с помощью isinf или isnan в качестве мертвого кода используйте эту опцию. По умолчанию анализ Bug Finder не включает бесконечности и NaNs.
НаАнализ позволяет бесконечности и NaNs. Например, в этом режиме:
Анализ принимает, что операции с плавающей точкой могут привести к таким результатам, как бесконечность и NaNs.
При помощи опций Infinities (-check-infinite) и NaNs (-check-nan)можно выбрать, чтобы подсветить операции, которые приводят к нефинитным результатам и остановить потоки выполнения, где происходят нефинитные результаты. Эти опции недоступны для анализа Bug Finder.
Анализ принимает, что переменные с плавающей точкой с неизвестными значениями могут иметь любое значение, разрешенное их типом, включая бесконечное или NaN. Переменные с плавающей точкой с неизвестными значениями включают изменчивые переменные и возвращаемые значения упрямых функций.
Off (по умолчанию)Анализ не допускает бесконечности и NaNs. Например, в этом режиме:
Анализ Code Prover производит красную проверку на операции с плавающей точкой, которая создает бесконечность или NaN как единственный возможный результат на всех путях выполнения. Эта верификация производит оранжевую проверку на операции с плавающей точкой, которая потенциально может привести к бесконечности или NaN.
Анализ Code Prover принимает, что переменные с плавающей точкой с неизвестными значениями являются полномасштабными, но конечными.
Анализ Bug Finder показывает сравнения с бесконечностью, используя isinf как мертвый код.
IEEE® 754 Стандарт позволяет специальные величины, такие как бесконечность и NaN чтобы вы могли обрабатывать определенные числовые исключения, не прерывая код. Некоторые реализации стандарта C поддерживают бесконечность и NaN.
Если ваш компилятор поддерживает бесконечности и NaNs и вы учитываете их явным образом в коде, используйте эту опцию, чтобы верификация также позволяла им.
Например, если деление приводит к бесконечности, в коде вы задаете альтернативное действие. Поэтому вы не хотите, чтобы верификация подсвечивала операции деления, которые приводят к бесконечности.
Если ваш компилятор поддерживает бесконечности и NaNs, но вы не уверены, что учитываете их явно в коде, используйте эту опцию, чтобы верификация включала бесконечности и NaNs. Используйте опции -check-nan и -check-infinite с аргументом warn так что верификация подсвечивает операции, которые приводят к бесконечности и NaNs, но не останавливает поток выполнения. Эти опции недоступны для анализа Bug Finder.
Если вы запускаете анализ Code Prover и используете эту опцию, проверки на переполнение, деление на нуль и другие численные ошибки времени выполнения отключаются. См. «Числовые проверки» (Polyspace Code Prover).
Если вы запускаете анализ Bug Finder и используете эту опцию:
Шашки для переполнения и деления на нули отключены. См. «Численные дефекты».
Шашечный Floating point comparison with equality operators может показать ложные срабатывания.
Если вы выберете эту опцию, количество и тип чеков Code Prover в вашем коде может измениться.
Например, в следующем примере, когда вы выбираете опцию, результаты имеют одну менее красную проверку и еще три зеленые проверки.
| Бесконечности и NaNS не разрешены | Бесконечности и допустимые NaNs |
|---|---|
Code Prover создает Division by zero ошибку и останавливает верификацию. double func(void) {
double x=1.0/0.0;
double y=1.0/x;
double z=x-x;
return z;
} | Если вы выбираете эту опцию, Code Prover не проверяет наличие Division by zero ошибки. double func(void) {
double x=1.0/0.0;
double y=1.0/x;
double z=x-x;
return z;
}Анализ принимает, что деление на ноль приводит к:
В результатах анализа в Polyspace® пользовательский интерфейс, если поместить курсор на |
Параметр: -allow-non-finite-floats |
| По умолчанию: Off |
Пример (Bug Finder):
Polyspace Bug Finder -sources file_name |
Пример (Code Prover):
Polyspace Code Prover -sources file_name |
Пример (Bug Finder Server):
polyspace-bug-finder-server -sources file_name |
Пример (Код Prover Server):
Полипространство -code-prover-server -sources file_name |
Infinities (-check-infinite) | NaNs (-check-nan) | Численные дефекты | Числовые проверки (Polyspace Code Prover)