-k-limiting)Ограничьте глубину анализа для вложенных структур
Эта опция влияет только на анализ Code Prover.
Задайте предел глубины анализа для вложенных структур.
Пользовательский интерфейс (только для настольных продуктов): В строении проекта опция доступна на узле Scaling.
Командная строка и файл опций: Используйте опцию -k-limiting. См. «Информация о командной строке».
Используйте эту опцию, если анализ медленный, потому что ваш код имеет структуру, которая имеет много уровней глубины.
Как правило, появляется предупреждающее сообщение, когда структура с глубокой иерархией замедляет верификацию.
По умолчанию: Анализируется полная глубина вложенных структур.
Введите число для определения глубины анализа вложенных структур. Например, если вы задаете 0, анализ не проверяет структуру внутри структуры.
Если вы задаете число менее 2, верификация может быть менее точной.
Параметр: -k-limiting |
Значение: |
Пример (Code Prover):
Polyspace Code Prover -sources file_name
|
Пример (Код Prover Server):
Полипространство -code-prover-server -sources file_name
|