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