Polyspace Code Prover™ доказывает отсутствие ошибок времени выполнения в исходном C и C++ коде – таких, как переполнение, деление на ноль, доступ за пределы массива и других . Результаты создаются без выполнения программы, инструментального оснащения кода или тестовых векторов. Polyspace Code Prover использует статический анализ и абстрактную интерпретацию, основанную на формальных методах. Инструмент можно использовать как с кодом, написанным вручную, так и с автоматически сгенерированным кодом, или на их комбинации. Каждая операция в коде расцвечивается для указания отсутствия ошибок времени выполнения, доказанных ошибок, недостижимых операций и недоказанных операций.Polyspace Code Prover™ доказывает отсутствие ошибок времени выполнения в исходном C и C++ коде – таких, как переполнение, деление на ноль, доступ за пределы массива и других . Результаты создаются без выполнения программы, инструментального оснащения кода или тестовых векторов. 
Polyspace Code Prover использует статический анализ и абстрактную интерпретацию, основанную на формальных методах. Инструмент можно использовать как с кодом, написанным вручную, так и с автоматически сгенерированным кодом, или на их комбинации. 
Каждая операция в коде расцвечивается для указания отсутствия ошибок времени выполнения, доказанных ошибок, недостижимых операций и недоказанных операций. Polyspace Code Prover также отображает информацию о диапазонах переменных и значениях, возвращаемых функциями, и может доказать условия, при которых переменные нарушают указанные диапазоны.
Результаты могут быть опубликованы в веб панель для отслеживания метрик качества и обеспечения соответствия целям качества программного обеспечения. Polyspace Code Prover может быть интегрирован с системами построения кода для автоматизированной верификации. 
Поддержка промышленных стандартов доступна с использованием IEC Certification Kit (для IEC 61508 и ISO 26262) и DO Qualification Kit (для DO-178). Также доступна поддержка языка Ada.

Ключевые особенности

  • Доказательство отсутствия определенных ошибок времени выполнения в C и C++ коде
  • Расцветка ошибок времени выполнения непосредственно в коде
  • Расчет диапазонов для переменных и значений, возвращаемых функциями
  • Идентификация переменных, нарушающих указанные диапазоны
  • Метрики качества для отслеживания соответствия целям качества программного обеспечения
  • Веб панель, представляющая метрики кода и состояние качества проекта
  • Управляемый процесс рассмотрения кода для классификации результатов и ошибок времени выполнения
  • Графическое представление операций чтения и записи в переменные

Системные требования


${message}

${message}