-check-nan
)Задайте, как обрабатывать операции с плавающей точкой, которые приводят к NaN
Эта опция влияет только на анализ Code Prover.
Задайте, как анализ должен обрабатывать операции с плавающей точкой, которые приводят к NaN.
Пользовательский интерфейс (только для настольных продуктов): В строении проекта опция находится на узле Check Behavior. Смотрите Зависимости для других опций, которые вы также должны включить.
Командная строка и файл опций: Используйте опцию -check-nan
. См. «Информация о командной строке».
Используйте эту опцию, чтобы включить обнаружение операций с плавающей точкой, которые приводят к NaN-s.
Если вы задаете, что анализ должен учитывать нефинитные поплавки, по умолчанию анализ не помечает эти операции. Используйте эту опцию, чтобы обнаружить эти операции, все еще включая нефинитные поплавки.
По умолчанию: allow
allow
Проверка операции не производится верификацией.
Например, в следующем коде нет Invalid operation on floats проверки.
double func(void) { double x=1.0/0.0; double y=x-x; return y; }
warn-first
Эта верификация производит проверку операции. Проверка определяет, является ли результат операции NaN, когда сами операнды не являются NaN. Например, проверка помечает операцию val1 + val2
только если результатом может быть NaN, когда оба val1
и val2
не являются NaN. Эта верификация не завершает поток выполнения, который создает NaN.
Если верификация обнаруживает операцию, которая создает NaN как единственный возможный результат на всех путях выполнения, и сами операнды никогда не являются NaN, проверка становится красной. Если операция потенциально может привести к NaN, проверка будет оранжевой.
Для образца в следующем коде существует проверка Invalid operation on floats без блокировки на NaN.
double func(void) { double x=1.0/0.0; double y=x-x; return y; }
Несмотря на то, что Invalid operation on floats проверяют -
операция красная, верификация продолжается. Например, зеленая проверка Non-initialized local variable появится на y
в return
оператор.
forbid
Эта верификация производит проверку операции и завершает поток выполнения, который создает NaN.
Если проверка окрашена красным цветом, верификация не будет продолжена для оставшегося кода в тех же возможностях, что и проверка. Если чек оранжевый, верификация продолжается, но удаляет из фактора значения переменных, которые создали NaN.
Например, в следующем коде существует блокировка Invalid operation on floats проверка на NaN.
double func(void) { double x=1.0/0.0; double y=x-x; return y; }
Верификация останавливается, потому что Invalid operation on floats проверяет -
операция красная. Например, проверка Non-initialized local variable не отображается на y
в return
оператор.
Проверка Invalid operation on floats на NaN также появляется на /
операция и зеленая.
Чтобы использовать эту опцию, вы должны включить режим верификации, который включает бесконечности и NaNs. См. Consider non finite floats (-allow-non-finite-floats)
.
Параметр: -check-nan |
Значение: allow | warn-first | forbid |
По умолчанию: allow |
Пример (Code Prover): Polyspace Code Prover -sources |
Пример (Код Prover Server):
Полипространство -code-prover-server -sources file_name |
Invalid operation on floats
(Polyspace Code Prover)