Polyspace ® Bug Finder™ и Polyspace Code Prover™ обнаружения ошибок во время выполнения с помощью статического анализа. Хотя продукты имеют схожий пользовательский интерфейс и математика, лежащая в основе анализа, иногда может быть одинаковой, цели двух продуктов различны.
Программа Bug Finder (или Polyspace as You Code, которая выполняет однофайловый анализ аналогично Bug Finder) быстро анализирует код и обнаруживает множество типов дефектов. Программа Code Prover проверяет каждую операцию в коде на наличие набора возможных ошибок времени выполнения и пытается доказать отсутствие ошибки для всех путей выполнения [1]. Например, для каждого деления в коде анализ проверки кода пытается доказать, что знаменатель не может быть нулевым. Bug Finder не выполняет такую исчерпывающую проверку. Например, Bug Finder также проверяет наличие деления по нулевой ошибке, но может не найти все операции, которые могут вызвать ошибку.
Два продукта включают различия в настройке, анализе и анализе результатов из-за этого различия в целях. В следующих разделах рассматриваются основные различия между функцией поиска ошибок и функцией проверки кода (также известной как проверка). В зависимости от требований можно включить один или оба вида анализа в соответствующие моменты жизненного цикла разработки программного обеспечения.
Более конкретные типы дефектов с помощью средства поиска ошибок
Упрощение процесса установки с помощью средства поиска ошибок
Меньше запусков для чистого кода с помощью средства поиска ошибок
Более строгий анализ потока данных и управления с помощью средства проверки кода
Несколько ложных срабатываний с помощью средства поиска ошибок
Регулярно используйте функцию поиска ошибок и программу проверки кода в процессе разработки. Продукты предоставляют уникальный набор возможностей и дополняют друг друга. Возможные способы совместного использования продуктов см. в разделе Workflow Using Both Bug Finder и Code Prover.
В этой таблице представлен обзор того, как продукты дополняют друг друга. Дополнительные сведения см. в разделах ниже.
| Особенность | Поиск ошибок | Проверка кода |
|---|---|---|
| Количество шашек | 309 | 30 проверок на наличие критических ошибок времени выполнения и 4 проверки использования глобальных переменных |
| Глубина анализа | Быстро. Например:
| Исчерпывающий. Например:
|
| Критерии отчетности | Вероятные дефекты | Доказанные результаты |
| Критерии обнаружения ошибок | Несколько ложных срабатываний | Ноль ложных негативов |
Насколько быстрее выполняется анализ Bug Finder, зависит от размера приложения. Время анализа Bug Finder линейно увеличивается с размером приложения. Время проверки Prover кода увеличивается со скоростью, превышающей линейную.
Одним из возможных рабочих процессов является запуск программы Code Prover для анализа модулей или библиотек на предмет устойчивости к определенным ошибкам и запуск программы Bug Finder на этапе интеграции. Анализ Bug Finder на больших кодовых базах может быть завершен за гораздо более короткое время, а также найти такие дефекты интеграции, как несоответствие деклараций и гонка данных.
Программа Code Prover пытается доказать отсутствие:
Ошибка деления на нуль для каждой операции деления или модуля
Ошибка индекса массива вне границ при каждом доступе к массиву
Неинициализированная ошибка переменной при каждом считывании переменной
Ошибка переполнения для каждой операции, которая может быть переполнена
и так далее.
Для каждой операции:
Если средство проверки кода может доказать отсутствие ошибки для всех путей выполнения, оно подсвечивает операцию зеленым цветом.
Если средство проверки кода может доказать наличие определенной ошибки для всех путей выполнения, оно выделяет операцию красным цветом.
Если средство проверки кода не может доказать отсутствие ошибки или наличие определенной ошибки, оно выделяет операцию оранжевым цветом. Этот небольшой процент проверок оранжевого цвета указывает на операции, которые необходимо тщательно проверить путем визуального осмотра или тестирования. Оранжевые проверки часто указывают на скрытые уязвимости. Например, операция может быть безопасной в текущем контексте, но может быть неуспешной при повторном использовании в другом контексте.
Для диагностики проверок можно использовать информацию, предоставленную в интерфейсе пользователя Polyspace. См. раздел Более строгий анализ потока данных и управления с помощью средства проверки кода. Можно также предоставить контекстную информацию, чтобы еще больше уменьшить число неподтвержденных кодов, например ограничить диапазоны ввода извне.
Bug Finder не стремится к исчерпывающему анализу. Он пытается обнаружить как можно больше ошибок и уменьшить количество ложных срабатываний. Для критически важных компонентов программного обеспечения запуска средства поиска ошибок недостаточно, поскольку, несмотря на устранение всех обнаруженных в анализе дефектов, во время выполнения кода все еще могут возникать ошибки (ложные негативы). После запуска программы проверки кода на вашем коде и решения найденных проблем, вы можете ожидать, что качество вашего кода будет намного выше. См. раздел Ноль ложных негативов с проверочным кодом.
Программа Code Prover проверяет типы ошибок времени выполнения, где можно математически доказать отсутствие ошибки. Помимо обнаружения ошибок, отсутствие которых может быть математически доказано, Bug Finder также обнаруживает другие дефекты.
Например, оператор if(a=b) семантически корректен по стандарту языка Си, но часто указывает на непреднамеренное присвоение. Bug Finder обнаруживает такие непреднамеренные операции. Хотя средство проверки кода не обнаруживает такие непреднамеренные операции, оно может обнаружить, если непреднамеренная операция вызывает другие ошибки во время выполнения.
Примеры дефектов, обнаруженных Bug Finder, но не Code Prover, включают в себя дефекты надлежащей практики, дефекты управления ресурсами, некоторые дефекты программирования, дефекты безопасности и дефекты объектно-ориентированного проектирования C++.
Дополнительные сведения см. в разделе:
Дефекты: список дефектов, которые может обнаружить Bug Finder.
Проверки времени выполнения: список ошибок времени выполнения, которые может обнаружить программа проверки кода.
Даже если код успешно создается в цепочке инструментов компиляции, это может привести к сбою на этапе компиляции проверки программы проверки кода. Строгая компиляция в Code Prover связана с её способностью доказывать отсутствие определённых ошибок времени выполнения.
Программа Code Prover строго следует стандарту ANSI ® C99 Standard, если явно не используются параметры анализа, эмулирующие компилятор.
Чтобы разрешить отклонения от стандарта ANSI C99 Standard, необходимо использовать опции. При создании проекта Polyspace из системы сборки параметры устанавливаются автоматически.
Средство проверки кода не позволяет связывать ошибки, разрешенные обычными компиляторами.
Хотя компилятор допускает ошибки связывания, такие как несоответствие сигнатуры функции между модулями компиляции, чтобы избежать неожиданного поведения во время выполнения, необходимо исправить ошибки.
Дополнительные сведения см. в разделе Устранение ошибок компиляции и связывания.
Bug Finder менее строг в отношении определенных ошибок компиляции. Ошибки связывания, такие как несоответствие в сигнатуре функции между различными модулями компиляции, могут остановить проверку средства проверки кода, но не анализ средства поиска ошибок. Поэтому можно выполнить анализ Bug Finder с меньшими усилиями по настройке. В Bug Finder ошибки связывания часто регистрируются как дефект после завершения анализа.
Чтобы гарантировать отсутствие определенных ошибок времени выполнения, программа Code Prover следует строгим правилам после обнаружения ошибки времени выполнения в операции. Как только возникает ошибка во время выполнения, состояние программы плохо определено, и средство проверки кода не может доказать отсутствие ошибок в последующем коде. Поэтому:
Если программа Code Prover доказывает наличие определенной ошибки и отображает красную проверку, она не проверяет остающийся код в том же блоке.
Исключения включают в себя проверки, такие как Переполнение (Overflow), где анализ продолжается с результатом переполнения либо усеченным, либо обернутым.
Если программа Code Prover подозревает наличие ошибки и отображает оранжевую проверку, она исключает из рассмотрения путь, содержащий ошибку. Например, если средство проверки кода обнаруживает ошибку Division by Zero в операции 1/x, в последующей операции на x в этом блоке, x не может быть нулевым.
Если средство проверки кода обнаруживает, что блок кода недоступен, и отображает серую проверку, оно не обнаруживает ошибок в этом блоке.
Дополнительные сведения см. в разделе Анализ проверки кода после проверки красного и оранжевого цветов.
Поэтому после исправления проверок красного и серого цвета и повторного запуска проверки можно найти дополнительные проблемы. Необходимо выполнить проверку несколько раз и каждый раз устранять неполадки для полностью чистого кода. Ситуация похожа на динамическое тестирование. При динамическом тестировании после устранения сбоя в определенной точке кода можно обнаружить новый сбой в последующем коде.
Bug Finder не останавливает весь анализ в блоке после обнаружения дефекта в этом блоке. Даже с помощью Bug Finder может потребоваться выполнить анализ несколько раз, чтобы получить полностью чистый код. Однако требуемое количество запусков меньше, чем у программы проверки кода.
Средство поиска ошибок показывает некоторые результаты анализа во время его выполнения. Для просмотра результатов не требуется ждать окончания анализа.
Программа проверки кода показывает результаты только после завершения проверки. Как только Bug Finder обнаружит дефект, он может отобразить дефект. Программа проверки кода должна доказать отсутствие ошибок на всех путях выполнения. Поэтому он не может отображать результаты во время анализа.
Для каждой операции в коде программа Code Prover предоставляет:
Подсказки, отображающие диапазон значений каждой переменной в операции.
Для указателя в подсказках отображается переменная, на которую указывает указатель, а также значения переменных.
Графическое представление последовательности вызова функции, которая приводит к операции.
Используя эту информацию диапазона и график вызовов, можно легко перемещаться по иерархии вызовов функций и понять, как переменная получает значения, которые приводят к ошибке. Например, для ошибки Out of Bounds Array Index можно найти, где индексной переменной сначала присваиваются значения, которые приводят к ошибке.
При просмотре результата в Bug Finder также имеется вспомогательная информация для понимания первопричины дефекта. Например, у вас есть трассировка, откуда Bug Finder обнаружил дефект к его первопричине. Однако в программе Code Prover имеется более полная информация, поскольку она помогает понять все пути выполнения кода.
Анализ потока данных в программе проверки кода
Анализ потока управления в программе проверки кода
Bug Finder нацелен на несколько ложных срабатываний, то есть результатов, которые вы вряд ли исправите. По умолчанию отображаются только те дефекты, которые могут быть наиболее значимыми для вас.
Bug Finder также присваивает типу дефекта атрибут, называемый воздействием, на основе критичности дефекта и частоты ложных срабатываний. Можно проанализировать код только на наличие серьезных дефектов. Можно также включить или отключить дефект, который не требуется просматривать [2].
Программа Code Prover предназначена для исчерпывающего анализа. Программа проверяет каждую операцию, которая может вызвать определенные типы ошибок. Если операция кода зеленая, это означает, что операция не может вызвать ошибки во время выполнения, которые программа проверила на наличие [3]. Таким образом, программное обеспечение стремится к нулю ложных негативов.
Если программа не может доказать отсутствие ошибки, она выделяет подозрительную операцию красным или оранжевым цветом и требует проверки операции.
Если у вас есть и Bug Finder, и Code Prover, основываясь на указанных выше различиях, вы можете соответствующим образом развернуть эти два продукта в рабочем процессе разработки программного обеспечения. Например:
Все разработчики в организации могут запускать Bug Finder на только что разработанном коде. Для поддержания стандартов в организации можно развернуть общую конфигурацию, которая ищет только определенные типы дефектов.
Программа Code Prover может быть развернута как часть пакета модульного тестирования.
Приложение Code Prover можно запускать только для критически важных компонентов проекта, а приложение Bug Finder - для всего проекта.
Можно запустить программу проверки кода на модулях кода на уровне модульного тестирования и запустить программу поиска ошибок при интеграции модулей.
Перед тестированием установки можно запустить программу проверки кода. Code Prover тщательно проверяет ваш код и пытается доказать наличие или отсутствие ошибок. Вместо записи модульных тестов для всего кода можно записать тесты только для неподтвержденного кода. Использование программы Code Prover перед модульным тестированием значительно сокращает ваши усилия по тестированию.
В зависимости от характера рабочего процесса разработки программного обеспечения и доступных ресурсов существует множество других способов включения двух видов анализа. Оба продукта можно запускать на рабочем столе во время разработки или в рамках автоматизированного тестирования на удаленном сервере. Обратите внимание, что проще интерпретировать и исправлять ошибки ближе к разработке. Использование обоих продуктов будет полезным, если они будут развертываться на ранних этапах и часто в процессе разработки.
Если на одном и том же коде выполняется поиск ошибок и проверка кода, существует два важных аспекта.
Оба продукта могут обнаруживать нарушения правил кодирования, таких как правила MISRA C ® и правила JSF ® C++.
Однако если вы хотите обнаружить только нарушения правил кодирования MISRA C:2012, используйте средство поиска ошибок. Bug Finder поддерживает все правила кодирования MISRA C:2012. Программа проверки кода не поддерживает несколько правил.
Если результат найден в анализе поиска ошибок и проверки кода, можно прокомментировать результат проверки ошибок и импортировать комментарий в программу проверки кода.
Например, большинство проверок правил кодирования являются общими для Bug Finder и Code Prover. Можно добавлять комментарии к нарушениям правил кодирования в Bug Finder и импортировать комментарии к тем же нарушениям в Code Prover. Чтобы импортировать комментарии, откройте результирующий набор и выберите Инструменты > Импортировать комментарии.
Один и тот же проект можно использовать как для поиска ошибок, так и для проверки кода. Следующий набор опций является общим для поиска ошибок и проверки кода:
При выполнении проверки программы проверки кода, возможно, потребуется изменить больше параметров по умолчанию, так как программа проверки кода строже подходит для ошибок компиляции и связывания.
[1] Для каждой операции в коде средство проверки кода рассматривает все пути выполнения, ведущие к операции, которые не имеют предыдущей ошибки. Если путь выполнения содержит ошибку перед операцией, средство проверки кода не учитывает ее. См. раздел Анализ проверки кода после проверки красного и оранжевого цветов.
[2] Можно также отключить некоторые дефекты программы проверки кода, связанные с отсутствием инициализации.
[3] Результат проверки кода сохраняется только в том случае, если код выполняется при тех же условиях, которые были предоставлены программе проверки кода с помощью опций анализа.