Продукты Polyspace ® проверяют код C, C++ и Ada, обнаруживая ошибки времени выполнения перед компиляцией и выполнением кода .
Для проверки исходного кода необходимо настроить параметры проверки в проекте, выполнить проверку и просмотреть результаты. Графический интерфейс пользователя позволяет эффективно просматривать результаты проверки. Программа присваивает цвет операциям в исходном коде следующим образом:
Зеленый - указывает на то, что операция не имеет определенных видов ошибок.
Красный (Red) - указывает на наличие в операции хотя бы одной ошибки.
Серый - указывает на недоступный код.
Оранжевый - указывает, что операция может иметь ошибку по некоторым путям выполнения.
Цветовое кодирование помогает быстро выявлять ошибки и находить точное местоположение ошибки в исходном коде. После исправления ошибок можно выполнить проверку повторно.
Проверка Polyspace может помочь вам:
Программное обеспечение Polyspace повышает надежность приложений C/C + +, проверяя правильность кода и выявляя ошибки во время выполнения. Используя расширенные методы проверки, программное обеспечение Polyspace выполняет полную проверку исходного кода.
Поскольку программное обеспечение Polyspace проверяет выполнение кода, оно может определить код, который:
Никогда не имеет ошибки
Всегда имеет ошибку
Недостижим
Возможно, произошла ошибка
Эта информация позволяет определить, какая часть кода не содержит ошибок во время выполнения, и повысить надежность кода можно путем исправления ошибок.
Вы также можете повысить качество кода, используя программное обеспечение проверки Polyspace для проверки соответствия кода установленным стандартам кодирования, таким как MISRA C ®, MISRA ® C++ или JSF ® C++. [1]
Программное обеспечение Polyspace сокращает время разработки, автоматизируя процесс проверки и помогая эффективно просматривать результаты проверки. Его можно использовать в любой момент процесса разработки. Однако использование его на ранних фазах кодирования позволяет находить ошибки, когда исправить их менее затратно.
Программное обеспечение Polyspace используется для проверки исходного кода перед компиляцией. Для проверки исходного кода необходимо настроить параметры проверки в проекте, выполнить проверку и просмотреть результаты. Этот процесс занимает значительно меньше времени, чем использование ручных методов или инструментов, требующих изменения кода или выполнения тестовых примеров.
Цветовое кодирование результатов помогает быстро выявлять ошибки. Вы потратите меньше времени на отладку, так как в исходном коде отображается точное местоположение ошибки. После исправления ошибок можно выполнить проверку повторно.
Программное обеспечение проверки Polyspace помогает эффективно использовать время. Поскольку вы знаете части кода, которые не имеют ошибок, вы можете сосредоточиться на коде с проверенными (красный код) или потенциальные ошибки (оранжевый код).
Проверка кода, который может иметь ошибки (оранжевый код), может занять много времени, но программное обеспечение Polyspace помогает в процессе проверки. Можно использовать фильтры, чтобы сосредоточиться на определенных типах ошибок, или можно разрешить программному обеспечению идентифицировать код, который следует просмотреть.
Программное обеспечение Polyspace упрощает обмен параметрами и результатами проверки, позволяя группе разработчиков работать вместе для повышения надежности изделия. После настройки параметров проверки разработчики могут повторно использовать их для других файлов в том же приложении.
Программное обеспечение проверки Polyspace поддерживает проверку кода на протяжении всего процесса разработки:
Индивидуальный разработчик может находить и исправлять ошибки времени выполнения на начальном этапе кодирования.
Инженеры по обеспечению качества могут проверить общую надежность приложения.
Менеджеры могут контролировать надежность приложений, генерируя отчеты по результатам проверки.
Программное обеспечение Polyspace использует статическую проверку для подтверждения отсутствия ошибок времени выполнения. Статическая проверка выводит динамические свойства программы без ее фактического выполнения. Это значительно отличается от других методов, таких как отладка во время выполнения, тем, что обеспечиваемая ею проверка не основана на данном тестовом случае или наборе тестовых случаев. Динамические свойства, полученные при проверке Polyspace, верны для всех исполнений программного обеспечения.
Статическая проверка является широким термином и применима к любому инструменту, который выводит динамические свойства программы без выполнения программы. Однако большинство статических средств проверки проверяют только сложность программного обеспечения при поиске конструкций, которые могут быть потенциально ошибочными. Проверка Polyspace обеспечивает проверку на глубоком уровне, выявляя почти все ошибки времени выполнения и возможные конфликты доступа с глобальными общими данными.
Проверка Полиспейса осуществляется путем аппроксимации проверяемого программного обеспечения, с использованием репрезентативных аппроксимаций операций программного обеспечения и данных.
Например, рассмотрим следующий код:
for (i=0 ; i<1000 ; ++i)
{ tab[i] = foo(i);
}Чтобы проверить, что переменная i никогда не переполняет диапазон tab, традиционным подходом было бы перечисление каждого возможного значения i. Потребуется тысяча проверок.
Используя метод статической проверки, переменная i моделируется по его доменной вариации. Например, модель i относится к статическому интервалу [0.. 999]. (В зависимости от сложности данных для этой цели также используются выпуклые многогранники, целочисленные решётки и более проработанные модели ).
По определению аппроксимация приводит к потере информации. Например, информация, которая i увеличивается на единицу при каждой потере цикла в цикле. Однако важным фактом является то, что эта информация не требуется для того, чтобы гарантировать отсутствие ошибки диапазона; необходимо только доказать, что изменение домена i меньше диапазона tab. Требуется только одна проверка, чтобы установить, что - и, следовательно, выигрыш в эффективности по сравнению с традиционными подходами.
Верификация статического кода имеет точное решение. Однако это точное решение нецелесообразно, поскольку оно потребует перечисления всех возможных контрольных случаев. В результате требуется аппроксимация для пригодного для использования инструмента.
Ничто не теряется с точки зрения полноты охвата. Причина в том, что проверка Polyspace работает, выполняя верхние аппроксимации. Другими словами, вычисленная вариационная область программной переменной является супернабором ее фактической вариационной области. В результате Polyspace проверяет элементы ошибок времени выполнения, которые требуют проверки.
[1] MISRA и MISRA C являются зарегистрированными товарными знаками MISRA Ltd., принадлежащими Консорциуму MISRA.