exponenta event banner

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

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

Описание

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

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

Задать опцию

Пользовательский интерфейс (только для настольных ПК): в конфигурации проекта опция доступна в узле Точность.

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

Зачем использовать этот параметр

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

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

Настройки

По умолчанию: Откл.

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

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

Совет

Эта опция используется только при наличии менее 1000 строк кода.

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

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