exponenta event banner

Уровень проверки (-to)

Укажите количество запусков процесса проверки кода

Описание

Этот параметр влияет только на анализ программы проверки кода.

Укажите количество запусков процесса проверки Polyspace ® в исходном коде. Каждый прогон может привести к большему количеству подтвержденных результатов, но также требует большего времени проверки.

Задать опцию

Пользовательский интерфейс (только для настольных ПК): в конфигурации проекта опция доступна в узле Точность.

файл командной строки и параметров: Использовать параметр -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 проходов, если вы не остановите ее вручную.

Совет

  • Используйте более высокий уровень проверки для меньшего количества оранжевых чеков.

    В некоторых случаях, если проверка может обнаружить, что результаты максимальной точности доступны после более раннего уровня, проверка прекращается и не переходит на указанный уровень.

     Разница между уровнями 0 и 1

    Если более высокий уровень проверки завершается неуспешно из-за нехватки памяти, но результаты доступны на более низком уровне, Polyspace отображает результаты с более низкого уровня.

  • Для получения наилучших результатов используйте опцию Software Safety Analysis level 2. Если проверка занимает слишком много времени, используйте более низкий уровень проверки. Исправьте красные ошибки и серый код перед повторным запуском проверки с более высоким уровнем проверки.

  • Использовать опцию 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 -sources file_name -to pass2
Пример (сервер проверки кода): polyspace-code-prover-server -sources file_name -to pass2

Можно также использовать следующие дополнительные значения, недоступные в интерфейсе пользователя:

  • 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 вместо этого.