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