Polyspace® Bug Finder™ и Polyspace Code Prover™ обнаруживают ошибки времени выполнения через статический анализ. Хотя продукты имеют подобный пользовательский интерфейс, и математика, лежащая в основе анализа, может иногда быть тем же самым, цели этих двух продуктов отличаются.
Bug Finder (или Polyspace, когда Вы Кодируете, который выполняет однофайловый анализ, похожий на Bug Finder) быстро анализирует ваш код и обнаруживает много типов дефектов. Code Prover проверяет каждую операцию в ваш код для набора возможных ошибок времени выполнения и пытается доказать отсутствие ошибки для всех путей к выполнению[1] . Например, для каждого деления в вашем коде, анализ Code Prover пытается доказать, что знаменатель не может быть нулем. Bug Finder не выполняет такую исчерпывающую верификацию. Например, Bug Finder также проверяет на ошибку деления на нуль, но он не может найти все операции, которые могут вызвать ошибку.
Эти два продукта включают различия в настройке, анализе и рассмотрении результатов, из-за этого различия в целях. В следующих разделах мы подсвечиваем первичные различия между Bug Finder и анализом Code Prover (также известный как верификацию). В зависимости от ваших требований можно включить один или оба вида исследований в соответствующих точках в жизненном цикле разработки программного обеспечения.
Используйте и Bug Finder и Code Prover регулярно в вашем процессе разработки. Продукты обеспечивают уникальный набор возможностей и дополнения друг друга. Для возможных способов использовать продукты вместе, смотрите, что Рабочий процесс Использует И Bug Finder и Code Prover.
Эта таблица предоставляет обзор как дополнение продуктов друг друга. Для получения дополнительной информации смотрите разделы ниже.
| Функция | Bug Finder | Code Prover |
|---|---|---|
| Количество средств проверки | 300 + средства проверки для дефектов | 30 проверок на критические ошибки времени выполнения и 4 проверяют использование глобальной переменной |
| Глубина анализа |
Быстро. Например:
|
Исчерпывающий. Например:
|
| Создание отчетов о критериях | Вероятные дефекты | Доказанные результаты |
| Критерии нахождения ошибки | Немного ложных срабатываний | Нет ложных срабатываний |
То, насколько быстрее анализ Bug Finder, зависит от размера приложения. Аналитическое время Bug Finder увеличивается линейно с размером приложения. Время верификации Code Prover увеличивается на уровне быстрее, чем линейный.
Один возможный рабочий процесс должен запустить Code Prover, чтобы анализировать модули или библиотеки для робастности против определенных ошибок и запустить Bug Finder на этапе интегрирования. Анализ Bug Finder больших кодовых баз может быть завершен в намного более короткое время, и также найти дефекты интегрирования, такие как Declaration mismatch и Data race.
Code Prover пытается доказать отсутствие:
Ошибка Division by Zero на каждом делении или операции модуля
Ошибка Out of Bounds Array Index на каждом доступе к массиву
Ошибка Non-initialized Variable на каждом переменном чтении
Ошибка Overflow на каждой операции, которая может переполниться
и так далее.
Для каждой операции:
Если Code Prover может доказать отсутствие ошибки для всех путей к выполнению, это подсвечивает операцию зеленого цвета.
Если Code Prover может доказать присутствие определенной ошибки для всех путей к выполнению, это подсвечивает операцию красного цвета.
Если Code Prover не может доказать отсутствие ошибки или присутствие определенной ошибки, это подсвечивает операцию в оранжевом. Этот небольшой процент оранжевых проверок указывает на операции, которые необходимо рассмотреть тщательно посредством визуального осмотра или тестирования. Оранжевые проверки часто указывают на скрытые уязвимости. Например, операция может быть безопасной в текущем контексте, но перестать работать, когда снова использовано в другом контексте.
Можно использовать информацию, предоставленную в пользовательском интерфейсе Polyspace, чтобы диагностировать проверки. Смотрите Более строгий Анализ Данных и Потока управления с Code Prover. Можно также предоставить контекстную информацию, чтобы уменьшать бездоказательный код еще больше, например, ограничить входные диапазоны внешне.
Bug Finder не стремится к исчерпывающему анализу. Это пытается обнаружить как можно больше ошибок и уменьшать ложные положительные стороны. Для критических компонентов программного обеспечения, запуская инструмент нахождения ошибки не достаточно, потому что несмотря на фиксацию всех дефектов нашел в анализе, у вас могут все еще быть ошибки во время выполнения кода (ложные отрицательные стороны). После рабочего Code Prover на вашем коде и решении найденных проблем, можно ожидать, что качество кода будет намного выше. Смотрите Нулевые Ложные Отрицательные стороны с Code Prover.
Code Prover проверяет на типы ошибок времени выполнения, где возможно математически доказать отсутствие ошибки. В дополнение к обнаружению ошибок, отсутствие которых может быть математически доказано, Bug Finder также обнаруживает другие дефекты.
Например, оператор if(a=b) семантически правильно согласно стандарту языка C, но часто указывает на непреднамеренное присвоение. Bug Finder обнаруживает такие непреднамеренные операции. Несмотря на то, что Code Prover не обнаруживает такие непреднамеренные операции, он может обнаружить, если непреднамеренная операция вызывает другие ошибки времени выполнения.
Примеры дефектов, обнаруженных Bug Finder, но не Code Prover, включают хорошие дефекты практики, дефекты управления ресурсами, некоторые дефекты программирования, дефекты безопасности, и дефекты в объекте C++ ориентировали проект.
Для получения дополнительной информации см.:
Дефекты: Список дефектов, которые может обнаружить Bug Finder.
Проверки на этапе выполнения (Polyspace Code Prover): Список ошибок времени выполнения, которые может обнаружить Code Prover.
Даже если ваш код создает успешно в вашем наборе инструментальных средств компиляции, он может перестать работать в фазе компиляции верификации Code Prover. Строгая компиляция в Code Prover связана со своей способностью доказать отсутствие определенных ошибок времени выполнения.
Code Prover строго следует за ANSI® Стандарт C99, если вы явным образом не используете опции анализа, которые эмулируют ваш компилятор.
Чтобы позволить отклонения от Стандарта ANSI C99, необходимо использовать Целевые и Параметры компилятора. Если вы создаете проект Polyspace из своей системы сборки, опции автоматически установлены.
Code Prover не позволяет соединять ошибки, которые могут разрешить общие компиляторы.
Хотя ваш компилятор разрешает соединять ошибки, такие как несоответствие в функциональной подписи между единицами компиляции, избегать неожиданного поведения во время выполнения, необходимо зафиксировать ошибки.
Для получения дополнительной информации смотрите Компиляцию Поиска и устранения неисправностей и Соединение Ошибок (Polyspace Code Prover).
Bug Finder менее строг об определенных ошибках компиляции. Соединение ошибок, таких как несоответствие в функциональной подписи между различными единицами компиляции, может остановить верификацию Code Prover, но не анализ Bug Finder. Поэтому можно запустить анализ Bug Finder с меньшим усилием по настройке. В Bug Finder о соединяющихся ошибках часто сообщают как дефект после того, как анализ будет завершен.
Чтобы гарантировать отсутствие определенных ошибок времени выполнения, Code Prover следует строгим правилам, если это обнаруживает ошибку времени выполнения в операции. Если ошибка времени выполнения происходит, состояние вашей программы неточно указано, и Code Prover не может доказать отсутствие ошибок в последующем коде. Поэтому:
Если Code Prover доказывает определенную ошибку и отображает красную проверку, он не проверяет остающийся код в том же блоке.
Исключения включают проверки, такие как Overflow, где анализ продолжает результат переполнения, или усеченного или перенесенного.
Если Code Prover подозревает присутствие ошибки и отображает оранжевую проверку, это устраняет путь, содержащий ошибку из фактора. Например, если Code Prover обнаруживает ошибку Division by Zero в операции 1/x, в последующей операции на x в том блоке, x не может быть нуль.
Если Code Prover обнаруживает, что блок кода недостижим и отображает серую проверку, это не обнаруживает ошибки в том блоке.
Для получения дополнительной информации смотрите, что Анализ Code Prover Следует за Красными и Оранжевыми Проверками (Polyspace Code Prover).
Поэтому, если вы фиксируете красные и серые проверки и повторно выполняете верификацию, можно найти больше проблем. Необходимо несколько раз запускать верификацию и устранять проблемы каждый раз для абсолютно чистого кода. Ситуация похожа на динамическое тестирование. В динамическом тестировании, если вы фиксируете отказ в определенный момент в коде, можно раскрыть новый отказ в последующем коде.
Bug Finder не останавливает целый анализ в блоке после того, как это найдет дефект в том блоке. Даже с Bug Finder, вам придется запустить анализ несколько раз, чтобы получить абсолютно чистый код. Однако количество требуемых запусков является меньше, чем Code Prover.
Bug Finder показывает некоторые результаты анализа, в то время как анализ все еще запускается. Вы не должны ожидать до конца анализа, чтобы рассмотреть результаты.
Code Prover показывает результаты только после конца верификации. Если Bug Finder находит дефект, он может отобразить дефект. Code Prover должен доказать отсутствие ошибок на всех путях к выполнению. Поэтому это не может отобразить результаты во время анализа.
Для каждой операции в вашем коде обеспечивает Code Prover:
Подсказки, показывающие область значений значений каждой переменной в операции.
Для указателя подсказки показывают переменную, что указатель указывает на, наряду со значениями переменных.
Графическое представление последовательности вызова функции, которая приводит к операции.
При помощи этой информации об области значений и графа вызовов, можно легко переместиться по иерархии вызова функции и изучить, как переменная получает значения, которые приводят к ошибке. Например, для ошибки Out of Bounds Array Index, можно найти, где индексная переменная является сначала присвоенными значениями, которые приводят к ошибке.
При рассматривании результата в Bug Finder у вас также есть информация о поддержке, чтобы изучить первопричину дефекта. Например, у вас есть traceback от того, где Bug Finder нашел дефект к своей первопричине. Однако в Code Prover, у вас есть больше полной информации, потому что информация помогает вам изучить все пути к выполнению в своем коде.
Анализ потока данных в Code Prover
Анализ потока управления в Code Prover
Bug Finder стремится к немногим ложным положительным сторонам, то есть, результаты, которые вы вряд ли зафиксируете. По умолчанию вам показывают только дефекты, которые, вероятно, будут самыми значимыми для вас.
Bug Finder также присваивает названный удар атрибута на дефектные типы на основе критичности дефекта и уровня ложных положительных сторон. Можно принять решение анализировать код только для дефектов высокого удара. Можно также включить или отключить дефект, который вы не хотите рассматривать[2] .
Code Prover стремится к исчерпывающему анализу. Программное обеспечение проверяет каждую операцию, которая может инициировать определенные типы ошибки. Если операция кода является зеленой, это означает, что операция не может вызвать те ошибки времени выполнения, на которые проверяло программное обеспечение[3] . Таким образом программное обеспечение стремится к нулевым ложным отрицательным сторонам.
Если программное обеспечение не может доказать отсутствие ошибки, это подсвечивает подозрительную операцию красного или оранжевого цвета и требует, чтобы вы рассмотрели операцию.
Bug Finder поддерживает современные внешние стандарты кодирования, такие как:
AUTOSAR C++ 14. См. C++ AUTOSAR 14 правил.
MISRA C:2012. См. директивы MISRA C:2012 и правила.
MISRA C ++:2008. См. MISRA C ++:2008 правил.
CERT C. Смотрите CERT C правила и рекомендации.
CERT C++. Смотрите CERT правила C++.
Поскольку Bug Finder быстрее и легче использовать, это - рекомендуемый инструмент, чтобы проверить соответствие этим внешним стандартам. Смотрите Поддержку Polyspace Кодирования Стандартов.
Даже при том, что Code Prover поддерживает подмножество предыдущих стандартов, он, в основном, предназначен для проверки ошибок времени выполнения. Исчерпывающий анализ Code Prover не требуется для обнаружения нарушений правила кодирования.
Если у вас есть и Bug Finder и Code Prover, на основе вышеупомянутых различий, можно развернуть эти два продукта соответственно в рабочем процессе разработки программного обеспечения. Например:
Все разработчики в вашей организации могут запустить Bug Finder на недавно разработанном коде. Для выпуска стандартов через вашу организацию можно развернуть общую настройку, которая только ищет определенные дефектные типы.
Code Prover может быть развернут как часть вашего набора модульного тестирования.
Можно запустить Code Prover только на критических компонентах проекта, в то время как рабочий Bug Finder на целом проекте.
Можно запустить Code Prover на модулях кода на уровне модульного тестирования и запустить Bug Finder при интеграции модулей.
Можно запустить Code Prover перед модульным тестированием. Code Prover исчерпывающе проверяет ваш код и пытается доказать присутствие или отсутствие ошибок. Вместо того, чтобы писать модульные тесты на ваш целый код, вы можете затем тесты записи только на бездоказательный код. Используя Code Prover, прежде чем модульное тестирование уменьшает ваши усилия по тестированию решительно.
В зависимости от природы вашего рабочего процесса разработки программного обеспечения и имеющихся ресурсов, существует много других способов, которыми можно включить два вида анализа. Можно запустить оба продукта на рабочем столе во время разработки или как часть автоматизированного тестирования на удаленном сервере. Обратите внимание на то, что легче интерпретировать и исправить ошибки ближе к разработке. Вы извлечете выгоду из использования обоих продуктов, если вы будете развертывать их рано и часто в вашем процессе разработки.
Существует два важных соображения, если вы запускаете и Bug Finder и Code Prover на том же коде.
Подмножество MISRA C® правила и JSF® Правила C++ могут проверяться и при помощи Bug Finder и при помощи Code Prover. Начиная в R2021b, Bug Finder является рекомендуемым инструментом для того, чтобы проверить соответствие кодированию стандартов. Bug Finder поддерживает большее количество кодирования правил. Например, Bug Finder поддерживает весь MISRA C:2012, кодирующий правила. Code Prover не поддерживает несколько правил.
Если результат найден и в Bug Finder и в анализе Code Prover, можно прокомментировать Bug Finder, заканчиваются и импортируют комментарий к Code Prover.
Например, большинство средств проверки правила кодирования характерно для Bug Finder и Code Prover. Можно добавить комментарии в кодирование нарушений правила в Bug Finder и импортировать комментарии к тем же нарушениям в Code Prover. Чтобы импортировать комментарии, откройте свой набор результатов и выберите Tools> Import Comments.
Можно использовать тот же проект и для Bug Finder и для анализа Code Prover. Следующий набор опций распространен между Bug Finder и Code Prover:
Вам придется изменить больше опций по умолчанию, когда вы запускаете верификацию Code Prover, потому что Code Prover более строг о компиляции и соединении ошибок.
[1] Для каждой операции в вашем коде Code Prover рассматривает все продвижение путей к выполнению к операции, которые не имеют предыдущей ошибки. Если путь к выполнению содержит ошибку до операции, Code Prover не рассматривает его. Смотрите, что Анализ Code Prover Следует за Красными и Оранжевыми Проверками (Polyspace Code Prover).
[2] Можно также отключить определенные дефекты Code Prover, связанные с неинициализацией.
[3] Результат Code Prover содержит, только если вы выполняете свой код при тех же условиях, которые вы предоставили к Code Prover через опции анализа.
