-O)Задайте уровень точности для верификации
Эта опция влияет только на анализ Code Prover.
Укажите уровень точности, который должна использовать верификация.
Пользовательский интерфейс (только для настольных продуктов): В строении проекта опция доступна на узле Precision.
Командная строка и файл опций: Используйте опцию -O , для образца, #-O0 или -O1. См. «Информация о командной строке».
Более высокая точность приводит к большему количеству проверенных результатов, но также требует большего времени верификации. Каждый уровень точности соответствует другому алгоритму, используемому для верификации.
В большинстве случаев вы видите оптимальный баланс между точностью и временем верификации на уровне 2.
По умолчанию: 2
0 Эта опция соответствует статической верификации интервала.
1 Эта опция соответствует более сложной статической верификации интервала.
2 Эта опция соответствует комплексной многогранной модели значений областей с дополнительной точностью для межпроцедурного анализа в зависимости от опции Improve precision of interprocedural analysis (-path-sensitivity-delta).
3
Эта опция подходит только для кода, имеющего менее 1000 линии. Используя эту опцию, процент проверенных результатов может быть очень высоким.
Для достижения наилучших результатов за разумное время используйте уровень по умолчанию 2. Если верификация занимает много времени, уменьшите точность. Однако число недоказанных проверок может увеличиться. Точно так же, чтобы уменьшить оранжевые проверки, вы можете улучшить свою точность. Но верификация может занять значительно больше времени.
Уровни точности 2 и ниже начинают принимать эффект только с уровней верификации выше Software Safety Analysis level 0. См. также Verification level (-to).
Например, чтобы уменьшить время анализа, вы, возможно, снизили уровень верификации до Software Safety Analysis level 0. Не пытайтесь уменьшить уровень точности ниже 2, чтобы уменьшить время анализа дальше.
Обратите внимание, что алгоритмы, используемые в уровне точности 3, могут также применяться к уровню верификации Software Safety Analysis level 0.
Параметр: -O0 | -O1 | -O2 | -O3 |
По умолчанию: -O2 |
Пример (Code Prover): Polyspace Code Prover -sources |
Пример (Код Prover Server):
Полипространство -code-prover-server -sources file_name |