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