Polyspace® Bug Finder™ и Polyspace Code Prover™ обнаруживать ошибки времени выполнения посредством статического анализа. Хотя продукты имеют аналогичный пользовательский интерфейс, и математика, лежащая в основе анализа, иногда может быть одинаковой, цели двух продуктов различны.
Bug Finder (или Polyspace as You Code, который выполняет анализ одного файла, подобный 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 |
|---|---|---|
| Количество шашек | 309 | 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. Смотрите более строгие данные и Поток управления анализ с Кодом 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 Standard, если вы явным образом не используете опции анализа, которые эмулируют ваш компилятор.
Чтобы разрешить отклонения от стандарта C99 ANSI, необходимо использовать опции Target и Compiler. Если вы создаете проект 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 у вас также есть вспомогательная информация, чтобы понять первопричину дефекта. Например, у вас есть трассировка, откуда Bug Finder нашел дефект своей первопричины. Однако в Code Prover у вас есть более полная информация, потому что информация помогает вам понять все пути выполнения в вашем коде.
Анализ потока данных в Code Prover
Управляйте анализом потока в Code Prover
Bug Finder нацелен на несколько ложных срабатываний, то есть результатов, которые вы вряд ли исправите. По умолчанию вам показываются только те дефекты, которые, вероятно, будут наиболее значимыми для вас.
Bug Finder также присваивает атрибут, называемый влиянием на типы дефектов, исходя из критичности дефекта и частоты ложных срабатываний. Вы можете принять решение анализировать свой код только на высокоимпактные дефекты. Можно также включить или отключить дефект, который не требуется просматривать[2] .
Code Prover стремится к исчерпывающему анализу. Программа проверяет каждую операцию, которая может вызвать определенные типы ошибок. Если операция кода является зеленой, это означает, что операция не может вызвать те ошибки времени выполнения, которые программное обеспечение проверяло на[3] . Таким образом, программное обеспечение стремится к нулю ложных срабатываний.
Если программа не может доказать отсутствие ошибки, она подсвечивает подозрительную операцию красным или оранжевым цветом и требует, чтобы вы пересмотрели операцию.
Если у вас есть 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++.
Однако, если вы хотите обнаружить MISRA C:2012 только нарушения правил кодирования, используйте Bug Finder. Bug Finder поддерживает все правила кодирования C:2012 MISRA. Code Prover не поддерживает несколько правил.
Если результат обнаружен как в анализе Bug Finder, так и в анализе Code Prover, можно прокомментировать результат Bug Finder и импортировать комментарий в Code Prover.
Для образца большинство шашек правил кодирования являются общими для Bug Finder и Кода 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 через опции анализа.
