-O)Укажите уровень точности для проверки
Этот параметр влияет только на анализ программы проверки кода.
Укажите уровень точности, который должен использоваться при проверке.
Пользовательский интерфейс (только для настольных ПК): в конфигурации проекта опция доступна в узле Точность.
файл командной строки и параметров: Использовать параметр -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 |
Пример (проверка кода): polyspace-code-prover -sources |
Пример (сервер проверки кода):
polyspace-code-prover-server -sources |
Specific precision (-modules-precision) | Verification level (-to)