-to
)Задайте число раз, процесс проверки работает на вашем коде
Эта опция влияет на анализ Программы автоматического доказательства Кода только.
Задайте число раз, процесс проверки Polyspace® работает на вашем исходном коде. Каждое выполнение может привести к большему количеству доказанных результатов, но также и требует большего количества времени верификации.
Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция доступна на узле Precision.
Командная строка: Используйте опцию -to
. Смотрите информацию о Командной строке.
Существует много причин, вы можете хотеть увеличить или уменьшить уровень верификации. Например:
Кодирующие правила проверяются рано во время фазы компиляции за некоторым исключением только. Если вы проверяете на кодирование одних только правил, можно понизить уровень верификации. Смотрите Проверку на Кодирование Стандартных Нарушений.
Если вы видите много оранжевых проверок после верификации, попытайтесь увеличить уровень верификации. Однако увеличение уровня верификации также увеличивает время верификации.
В большинстве случаев вы видите оптимальный баланс между точностью и время верификации на уровне 2.
Значение по умолчанию: Software Safety Analysis level 2
Source Compliance Checking
Polyspace завершает проверку правил кодирования в конце фазы компиляции.
Software Safety Analysis level 0
Процесс проверки запускается однажды на вашем исходном коде.
Software Safety Analysis level 1
Процесс проверки запускается дважды на вашем исходном коде.
Software Safety Analysis level 2
Процесс проверки запускается в три раза на вашем исходном коде. Используйте эту опцию для большинства точных результатов в соответствующее время.
Software Safety Analysis level 3
Процесс проверки запускается четыре раза на вашем исходном коде.
Software Safety Analysis level 4
Процесс проверки запускается пять раз на вашем исходном коде.
other
Если вы будете использовать эту опцию, верификация Polyspace сделает 20 передач, если вы не остановите его вручную.
Используйте более высокий уровень верификации для меньшего количества оранжевых проверок.
Если более высокий уровень верификации перестал работать, потому что верификация исчерпывает память, но результаты доступны на более низком уровне, Polyspace отображает результаты более низкого уровня.
Для лучших результатов используйте опцию Software Safety Analysis level 2
. Если верификация занимает слишком много времени, используйте более низкий Verification level. Зафиксируйте красные ошибки и код Грея прежде, чем повторно выполнить верификацию с более высокими уровнями верификации.
Используйте опцию Other
экономно, поскольку это может увеличить время верификации неблагоразумной суммой. Используя Software Safety Analysis level 2
обеспечивает оптимальную верификацию вашего кода в большинстве случаев.
Если Verification Level установлен в Source Compliance Checking
, не запускайте верификацию на удаленном сервере. Исходная проверка соответствия или компиляция, фаза происходит на вашем локальном компьютере так или иначе. Поэтому, если вы запускаете верификацию только в конец компиляции, верификации выполнения на вашем локальном компьютере.
Параметр: -to |
Значение: compile | pass0 | pass1 | pass2 | pass3 | pass4 | other |
Значение по умолчанию: pass2 |
Пример (программа автоматического доказательства кода):
|
Пример (сервер программы автоматического доказательства кода):
|
Можно также использовать эти дополнительные значения, не доступные в пользовательском интерфейсе:
C проекты: c-to-il
(C к фазе преобразования промежуточного языка)
Проекты C++: cpp-to-il
(C++ к фазе преобразования промежуточного языка), cpp-normalize
(фаза нормализации C++), cpp-link
(фаза ссылки C++)
Используйте эти значения, только если у вас есть определенные причины сделать так. Например, чтобы сгенерировать пустой ограничительный шаблон (DRS) для проектов C++, необходимо запустить анализ до фазы cpp-normalize
.