-O)Задайте уровень точности для верификации
Эта опция влияет на анализ Программы автоматического доказательства Кода только.
Задайте уровень точности, который должна использовать верификация.
Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция доступна на узле Precision.
Командная строка и файл опций: Используйте опцию-O, например, #-O0 или -O1. Смотрите информацию о командной строке.
Более высокая точность приводит к большему количеству доказанных результатов, но также и требует большего количества времени верификации. Каждый уровень точности соответствует различному алгоритму, используемому для верификации.
В большинстве случаев вы видите оптимальный баланс между точностью и время верификации на уровне 2.
Значение по умолчанию: 2
Эта опция соответствует статической верификации интервала.
Эта опция соответствует более комплексной статической верификации интервала.
Эта опция соответствует комплексной модели многогранника значений домена с дополнительной точностью для межпроцедурного анализа в зависимости от опции Improve precision of interprocedural analysis (-path-sensitivity-delta).
Эта опция только подходит для кода, имеющего меньше чем 1 000 линий. Используя эту опцию, процент доказанных результатов может быть очень высоким.
Для лучших результатов в соответствующее время используйте уровень по умолчанию 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 |
Пример (Программа автоматического доказательства Кода): Polyspace Code Prover - источники |
Пример (Сервер Программы автоматического доказательства Кода):
сервер программы автоматического доказательства полипробела кода - источники |
Specific precision (-modules-precision) | Verification level (-to)