Verification time limit (-timeout)

Задайте ограничение по времени на своей верификации

Описание

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

Задайте ограничение по времени для верификации в часах. Если верификация не завершается в том пределе, она останавливается.

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

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

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

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

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

По умолчанию, если внутренний шаг в верификации длится больше 24 часов, остановок верификации. Можно использовать эту опцию, чтобы уменьшать ограничение по времени еще больше. Обратите внимание на то, что у вас могут быть результаты верификации несмотря на таймаут верификации. Например, если шаг на Аналитическом уровне 1 Безопасности программного обеспечения испытывает таймаут, вы все еще получаете результаты уровня 0. Смотрите Verification level (-to).

Опция полезна только в очень конкретных случаях. Предположим, что ваш код имеет определенные построения, которые могут замедлить верификацию. Чтобы проверять это, можно наложить ограничение по времени на верификацию так, чтобы верификация остановилась, если это занимает слишком много времени.

Как правило, Техническая поддержка просит, чтобы вы использовали эту опцию по мере необходимости.

Настройки

Введите время в часах. Для частей часа задайте десятичную форму.

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

Параметр: -timeout
Значение: time
Пример (Программа автоматического доказательства Кода): Polyspace Code Prover - источники file_name - тайм-аут 5.75
Пример (Сервер Программы автоматического доказательства Кода): сервер программы автоматического доказательства полипробела кода - источники file_name - тайм-аут 5.75