Чтобы задать глобальные предположения об определенном построении кода, используйте опции предположения верификации. Например, укажите, что всеми внешними указателями может возможно быть 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® в пользовательском интерфейсе Polyspace, других IDE-s или скриптах.
