После верификации, Polyspace® Code Prover™ подсвечивает операции в коде с определенными цветами в зависимости от того, может ли операция вызвать ошибку времени выполнения. Смотрите Результаты Code Prover и Цвета исходного кода.
Не сразу ясно, почему верификация подсвечивает определенную операцию в красном (определенная ошибка времени выполнения) или оранжевом (потенциальная ошибка времени выполнения). Даже если понять причину ошибки, не сразу понятно, где ее исправить.
Часто ошибка времени выполнения в определенной операции связана с предыдущими операциями в вашем коде.
Например, операция переполнена из-за большого значения операнда, но операнд получает это значение в предыдущих операциях.
Чтобы выяснить, как предыдущая операция вызывает ошибку времени выполнения в текущей операции, выполните следующее:
Просмотрите сообщение, связанное с результатом верификации текущей операции.
Сообщение появится на панели Result Details или в всплывающих подсказках операции на панели Source. Сообщение показывает, как исследовать результат дальше.
Например, сообщение ниже показывает, что правый операнд может быть нулем. Чтобы определить, как переменная operand получает нулевое значение, необходимо просмотреть предыдущие операции, которые записывают в переменную.
Просмотрите в коде предыдущие операции, связанные с текущей операцией.
Пользовательский интерфейс Polyspace обеспечивает функции для легкой навигации между конкретными точками в коде. Например, вы можете переходить от имени функции к определению функции.
Определите подходящее место в коде, где можно реализовать исправление.
Для получения дополнительной информации о том, как просмотреть каждый тип проверки, смотрите Code Prover Run-Time Checks.
Если вы не предоставляете полное приложение или внешнюю информацию, необходимую для верификации, программное обеспечение должно делать определенные предположения относительно отсутствующего кода или внешней информации.
Например, если вы не предоставляете main функция, программное обеспечение генерирует main который вызывает только незакрытые функции. Если func1 вызывает func2, сгенерированный main не вызывает func2 снова. Эта верификация проверяет наличие ошибок времени выполнения в func2 только из контекста вызова в func1.
Предположения таковы, что они применяются к большинству приложений. Однако в нескольких случаях предположения по умолчанию могут не описать ваше окружение во время выполнения точно. Если предположения не те, которые вы ожидаете, результаты верификации могут оказаться неожиданными.
Проверьте, можно ли проследить результат верификации до допущения программного обеспечения. Частичный список допущений см. в разделе Допущения анализа Code Prover. Дополнительный список допущений приведен в codeprover_limitations.pdf в polyspaceroot\ polyspace\verifier\code _ prover _ рабочий стол
Часто можно изменить допущения по умолчанию с помощью определенных опций.
Цель и компилятор: Убедитесь, что вы должны задать опцию, чтобы эмулировать поведение компилятора.
Например, если необходимо, чтобы частные операций деления округлились, а не округлились, используйте опцию Division round down (-div-round-down).
Входы и упрямство: посмотрите, придется ли вам внешне ограничивать некоторые переменные.
Например, если необходимо ограничить глобальную переменную в определенной области значений, используйте опцию Constraint setup (-data-range-specifications).
Многозадачность: Если вы забыли указать некоторые задачи или механизмы защиты.
Например, если вы хотите задать, что функция представляет собой прерывание, не подлежащее предопределению, используйте опцию Interrupts (-interrupts).
Верификация Code Prover: Если вы проверяете модуль без main, увидеть, сгенерирован ли main инициализирует ваши глобальные переменные и вызывает ваши функции в правильном порядке.
Например, если вы хотите сгенерировать main чтобы вызвать все свои функции, используйте опцию Functions to call (-main-generator-calls) с аргументом all.
Предположения верификации: Проверьте, соответствуют ли допущения глобальной верификации вашему окружению во время выполнения.
Например, если необходимо, чтобы в верификации учитывалось, что неизвестные указатели могут быть NULL-значен, используйте опцию Consider environment pointers as unsafe (-stubbed-pointers-are-unsafe).
Проверяйте поведение: Убедитесь, что спецификации проверки во время выполнения подходят для вашего окружения во время выполнения.
Например, если вы хотите Illegally dereferenced pointer проверяйте, чтобы разрешить арифметику указателя между полями структуры, используйте опцию Enable pointer arithmetic across fields (-allow-ptr-arith-on-struct).
Если вы все еще не можете понять свой результат, обратитесь в MathWorks® Техническая поддержка для помощи в интерпретации вашего результата. Если вы не можете поделиться своими фактическими результатами верификации, предоставьте только определенную важную информацию о своем результате. Обратитесь в службу технической поддержки о проблемах с выполняемым Polyspace.
