-path-sensitivity-delta)Избегайте определенных приближений верификации для кода с меньшим количеством линий
Эта опция влияет только на анализ Code Prover.
Для меньшего кода используйте эту опцию, чтобы улучшить точность кросс-функционального анализа.
Пользовательский интерфейс (только для настольных продуктов): В строении проекта опция доступна на узле Precision.
Командная строка и файл опций: Используйте опцию -path-sensitivity-delta. См. «Информация о командной строке».
Используйте эту опцию, чтобы избежать определенных приближений на путях выполнения. Избегание этих приближений приводит к меньшему количеству оранжевых проверок, но гораздо больше времени верификации.
Например, для иерархий глубоких вызовов функций или вложенных условных операторов, чтобы завершить верификацию за разумное время, программное обеспечение объединяет много путей выполнения и хранит меньше информации на каждом этапе верификации. Если вы используете эту опцию, программное обеспечение хранит больше информации о путях выполнения, что приводит к более точной верификации.
По умолчанию: Off
Введите положительное целое число, чтобы включить эту опцию.
Ввод более высокого значения приводит к большему количеству проверенных результатов, но также увеличивает время верификации в геометрической прогрессии. Для образца значение 10 может привести к очень длительным временам верификации.
Используйте эту опцию только, когда у вас меньше 1000 строк кода.
Параметр: -path-sensitivity-delta |
| Значение: Положительное целое число |
Пример (Code Prover): Polyspace Code Prover -sources |
Пример (Код Prover Server):
Полипространство -code-prover-server -sources file_name |