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