Изучите результаты верификации

Проблема

После верификации Polyspace® Code Prover™ подсвечивает операции в вашем коде с определенными цветами в зависимости от того, может ли операция вызвать ошибку времени выполнения. Смотрите Цвета Результата и Исходного кода Программы автоматического доказательства Кода.

Это не сразу понятно, почему верификация подсвечивает определенную операцию красного цвета (определенная ошибка времени выполнения) или оранжевый (потенциальная ошибка времени выполнения). Даже если вы изучаете причину ошибки, это не сразу понятно, где зафиксировать его.

Возможная причина: отношение к предшествующим операциям кода

Часто ошибка времени выполнения в определенной операции связана с предшествующими операциями в вашем коде.

Например, операция переполняется из-за большого значения операнда, но операнд получает то значение в предыдущих операциях.

Решение

Чтобы заняться расследованиями, как предшествующая операция инициировала ошибку времени выполнения в текущей операции, сделайте следующее:

  • Просмотрите сообщение, сопоставленное с результатом верификации на текущей операции.

    Сообщение появляется в панели Result Details или в подсказках на операции в панели Source. Сообщение показывает вам, как исследовать результат далее.

    Например, сообщение ниже показов, что правильный операнд может быть нулем. Чтобы определить, как переменная операнда получает нуль значения, необходимо просмотреть предыдущие операции, которые пишут в переменную.

  • Просмотрите предшествующие операции в своем коде, которые связаны с текущей операцией.

    Пользовательский интерфейс Polyspace обеспечивает функции простой навигации между отдельными моментами в вашем коде. Например, можно перейти от имени функции до функционального определения.

Идентифицируйте подходящее место в своем коде, где можно реализовать фиксацию.

Дополнительные сведения о том, как рассмотреть каждый тип проверки см. в Проверках на этапе выполнения Программы автоматического доказательства Кода.

Возможная причина: предположения программного обеспечения

Если вы не предоставляете свое законченное приложение или внешнюю информацию, запрошенную для верификации, программное обеспечение должно сделать определенные предположения о недостающем коде или внешней информации.

Например, если вы не обеспечиваете main функция, программное обеспечение генерирует main это вызывает только невостребованные функции. Если func1 вызовы func2, сгенерированный main не вызывает func2 снова. Верификация проверяет на ошибки времени выполнения в func2 только от контекста вызова в func1.

Предположения таковы, что они применяются к большинству приложений. Однако в нескольких случаях, предположения по умолчанию не могут описать вашу среду выполнения точно. Если предположения не то, что вы ожидаете, результаты верификации могут быть неожиданными.

Решение

Смотрите, можно ли проследить результат верификации до предположения программного обеспечения. Для частичного списка предположений смотрите Аналитические Предположения Программы автоматического доказательства Кода. Дополнительный список предположений предоставлен в codeprover_limitations.pdf в polyspaceroot\polyspace\verifier\code_prover_desktop.

Часто, можно изменить предположения по умолчанию с помощью определенных опций.

Если вы все еще не можете изучить свой результат, свяжитесь с MathWorks® Technical Support для справки с интерпретацией вашего результата. Если вы не можете совместно использовать свои фактические результаты верификации, предоставьте только определенную важную информацию о своем результате. Смотрите Техническую поддержку Контакта.