-O)Задайте уровень точности для верификации
Эта опция влияет на анализ Программы автоматического доказательства Кода только.
Задайте уровень точности, который должна использовать верификация.
Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция доступна на узле Precision.
Командная строка: Используйте опцию -O#-O0 или -O1. Смотрите информацию о Командной строке.
Более высокая точность приводит к большему количеству доказанных результатов, но также и требует большего количества времени верификации. Каждый уровень точности соответствует различному алгоритму, используемому для верификации.
В большинстве случаев вы видите оптимальный баланс между точностью и время верификации на уровне 2.
Значение по умолчанию: 2
Эта опция соответствует статической верификации интервала.
Эта опция соответствует комплексной модели многогранника значений домена.
Эта опция соответствует более комплексным алгоритмам, тесно моделируя значения домена. Алгоритмы комбинируют и комплексные многогранники и целочисленные решетки.
Эта опция только подходит для кода, имеющего меньше чем 1 000 строк. Используя эту опцию, процент доказанных результатов может быть очень высоким.
Для лучших результатов в соответствующее время используйте уровень по умолчанию 2. Если верификация занимает много времени, уменьшайте точность. Однако количество бездоказательных проверок может увеличиться. Аналогично, чтобы уменьшать оранжевые проверки, можно улучшить точность. Но верификация может занять значительно более длительное время.
Параметр: -O0 | -O1 | -O2 | -O3 |
Значение по умолчанию: -O2 |
Пример (программа автоматического доказательства кода): |
Пример (сервер программы автоматического доказательства кода):
|