-to)Задайте количество раз, когда процесс верификации запускается на вашем коде
Эта опция влияет только на анализ Code Prover.
Задайте количество раз, когда 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 function) и распространяется на листья иерархии вызовов.
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 |
Пример (Code Prover): Polyspace Code Prover -sources |
Пример (Код Prover Server):
Полипространство -code-prover-server -sources file_name |
Можно также использовать следующие дополнительные значения, недоступные в пользовательском интерфейсе:
C проекты: c-to-il (C в фазу преобразования промежуточного языка)
C++ проекты: cpp-to-il (C++ в фазу преобразования промежуточного языка), cpp-normalize (компиляция C++), cpp-link (компиляция C++)
Используйте эти значения только при наличии определенных причин. Например, чтобы сгенерировать пустой шаблон ограничений (DRS) для проектов C++, запустите анализ до компиляции при помощи cpp-link или cpp-normalize.
Значения cpp-link и cpp-normalize будет удалено в следующем релизе. Использование compile вместо этого.
