-to)Задайте число раз, процесс проверки работает на вашем коде
Эта опция влияет на анализ Программы автоматического доказательства Кода только.
Задайте число раз, процесс проверки Polyspace® работает на вашем исходном коде. Каждый запуск может привести к большему количеству доказанных результатов, но также и требует большего количества времени верификации.
Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция доступна на узле Precision.
Командная строка: Используйте опцию -to. Смотрите информацию о командной строке.
Существует много причин, вы можете хотеть увеличить или уменьшить уровень верификации. Например:
Кодирующие правила проверяются рано во время фазы компиляции за некоторым исключением только. Если вы проверяете на кодирование одних только правил, можно понизить уровень верификации. Смотрите Проверку на Кодирование Стандартных Нарушений.
Если вы видите много оранжевых проверок после верификации, попытайтесь увеличить уровень верификации. Однако увеличение уровня верификации также увеличивает время верификации.
В большинстве случаев вы видите оптимальный баланс между точностью и время верификации на уровне 2.
Значение по умолчанию: Software Safety Analysis level 2
Source Compliance Checking Polyspace проверяет на ошибки компиляции только. Большинство нарушений правила кодирования также найдено в этой фазе.
Software Safety Analysis level 0 Процесс проверки выполняет некоторый простой анализ. Анализ спроектирован, чтобы достигнуть завершения несмотря на сложности в коде.
Если верификация застревает в более высоком уровне, попытайтесь запуститься к этому уровню и рассмотрите результаты.
Software Safety Analysis level 1 Процесс проверки анализирует каждую функцию однажды с алгоритмами, сложность которых зависит на уровне точности. Смотрите Precision level (-O). Анализ начинает с верхней части иерархии вызова функции (фактический или сгенерированный main функция), и распространяет к листам иерархии вызова.
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, не запускайте верификацию на удаленном сервере. Исходная проверка податливости или компиляция, фаза происходит на вашем локальном компьютере так или иначе. Поэтому, если вы запускаете верификацию только в конец компиляции, верификации запуска на вашем локальном компьютере.
Если вы хотите видеть, что глобальная переменная совместно использовать и использование только использует Show global variable sharing and usage only (-shared-variables-mode) запускать менее обширный анализ.
Параметр: -to |
Значение: compile | pass0 | pass1 | pass2 | pass3 | pass4 | other |
Значение по умолчанию: pass2 |
Пример (Программа автоматического доказательства Кода): Polyspace Code Prover - источники |
Пример (Сервер Программы автоматического доказательства Кода):
сервер программы автоматического доказательства полипробела кода - источники |
Можно также использовать эти дополнительные значения, не доступные в пользовательском интерфейсе:
C проекты: c-to-il (C к фазе преобразования промежуточного языка)
Проекты C++: cpp-to-il (C++ к фазе преобразования промежуточного языка), cpp-normalize (Фаза нормализации C++), cpp-link (Фаза ссылки C++)
Используйте эти значения, только если у вас есть определенные причины сделать так. Например, чтобы сгенерировать пустой ограничительный шаблон (DRS) для проектов C++, необходимо запустить анализ до cpp-normalize фаза.
