Чтобы задать глобальные допущения относительно конкретной конструкции кода, используйте опции допущений проверки. Например, укажите, что все внешние указатели могут быть NULL или volatile необходимо учитывать квалификатор для всех полей структуры. Для локальных предположений, применимых к определенным переменным, функциям или файлам, используйте опции Входы и заглушки (Inputs & Stubbing).
Более полный список допущений см. в разделе Допущения анализа проверочных кодов.
Respect types in fields (-respect-types-in-fields) | Не приводить к указателям не указательные поля структуры |
Respect types in global variables (-respect-types-in-globals) | Не выводить глобальные переменные, не указывающие на указатели |
Float rounding mode (-float-rounding-mode) | Определение режимов округления, учитываемых при определении результатов арифметики с плавающей запятой |
Consider environment pointers as unsafe (-stubbed-pointers-are-unsafe) | Укажите, что указатели среды могут быть небезопасными для отмены привязки, если не установлено иное |
Consider volatile qualifier on fields (-consider-volatile-qualifier-on-fields) | Предположим, что volatile квалифицированные поля структуры могут иметь все возможные значения в любой точке кода |
Задать параметры анализа в пространстве
Задайте параметры анализа Polyspace ® в интерфейсе пользователя Polyspace, других среде IDE или сценариях.