Чтобы задать глобальные допущения о определенной конструкции кода, используйте опции допущения верификации. Например, укажите, что все внешние указатели могут быть NULL или volatile необходимо учитывать квалификатор для всех структурных полей. Для локальных допущений, которые применяются к определенным переменным, функциям или файлам, используйте опции Inputs & Stubbing.
Для получения более полного списка допущений смотрите Допущения анализа Code Prover.
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) | Задайте, что указатели окружения могут быть небезопасны для dereference, если не ограничено иное |
Consider volatile qualifier on fields (-consider-volatile-qualifier-on-fields) | Предположим, что volatile поля квалифицированной структуры могут иметь все возможные значения в любой точке кода |
Задайте опции анализа Polyspace
Задайте Polyspace® опции анализа в пользовательском интерфейсе Polyspace, других IDE-s или скриптах.
