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