Чтобы задать глобальные предположения об определенном построении кода, используйте опции предположения верификации. Например, укажите, что всеми внешними указателями может возможно быть NULL или volatile спецификатор на всех полях структуры должен быть рассмотрен. Для локальных предположений, которые применяются к определенным переменным, функциям или файлам, используют Входные параметры и Блокирующие опции.
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
Объедините специфичные для проекта опции, такие как источники с допускающими повторное использование опциями, такими как средства проверки.
