Depth of verification inside structures (-k-limiting)

Ограничьте глубину анализа для вложенных структур

Описание

Эта опция влияет на анализ Программы автоматического доказательства Кода только.

Задайте предел глубине анализа для вложенных структур.

Установите опцию

Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция доступна на узле Scaling.

Командная строка и файл опций: Используйте опцию -k-limiting. Смотрите информацию о командной строке.

Почему использование эта опция

Используйте эту опцию, если анализ является медленным, потому что ваш код имеет структуру, которая является многими уровнями глубоко.

Как правило, вы видите предупреждающее сообщение, когда структура с глубокой иерархией замедляет верификацию.

Настройки

Значение по умолчанию: Вся глубина вложенных структур анализируется.

Введите номер, чтобы задать глубину анализа для вложенных структур. Например, если вы задаете 0, анализ не проверяет структуру в структуре.

Если вы задаете номер меньше чем 2, верификация могла бы быть менее точной.

Информация о командной строке

Параметр: -k-limiting
Значение: positive integer
Пример (Программа автоматического доказательства Кода): Polyspace Code Prover - источники file_name - k-ограничение 3
Пример (Сервер Программы автоматического доказательства Кода): сервер программы автоматического доказательства полипробела кода - источники file_name - k-ограничение 3

Смотрите также