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