Улучшите точность межпроцедурного анализа (-path-sensitivity-delta)

Избегайте определенных приближений верификации для кода с меньшим количеством строк

Описание

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

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

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

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

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

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

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

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

Настройки

Значение по умолчанию: 'off'

Введите положительное целое число, чтобы включить эту опцию.

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

Советы

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

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

Параметр: -path-sensitivity-delta
Значение: Положительное целое число
Пример (программа автоматического доказательства кода): polyspace-code-prover -sources file_name -path-sensitivity-delta 1
Пример (сервер программы автоматического доказательства кода): polyspace-code-prover-server -sources file_name -path-sensitivity-delta 1