После проверки Polyspace ® Code Prover™ выделяет операции в коде определенными цветами в зависимости от того, может ли операция вызвать ошибку во время выполнения. См. раздел Результат проверки кода и Цвета исходного кода.
Не сразу понятно, почему проверка выделяет определенную операцию красным (определенная ошибка времени выполнения) или оранжевым (потенциальная ошибка времени выполнения) цветом. Даже если понять причину ошибки, не сразу понятно, где ее исправить.
Часто ошибка во время выполнения конкретной операции связана с предыдущими операциями в коде.
Например, операция переполняется из-за большого значения операнда, но операнд получает это значение в предыдущих операциях.
Чтобы выяснить, как предыдущая операция вызывает ошибку времени выполнения в текущей операции, выполните следующие действия.
Просмотр сообщения, связанного с результатом проверки текущей операции.
Сообщение появляется на панели Сведения о результате (Result Details) или в подсказках по операции на панели Источник (Source). В этом сообщении показано, как исследовать результат дальше.
Например, сообщение ниже показывает, что правильный операнд может быть равен нулю. Чтобы определить, как переменная операнда получает нулевое значение, необходимо просмотреть предыдущие операции, которые записывают в переменную.
Просмотрите предыдущие операции в коде, связанные с текущей операцией.
Интерфейс пользователя Polyspace обеспечивает удобную навигацию между определенными точками в коде. Например, можно перейти от имени функции к определению функции.
Определите подходящее место в коде, где можно реализовать исправление.
Дополнительные сведения о проверке каждого типа проверки см. в разделе Проверки времени выполнения программы проверки кода.
Если вы не предоставите полное приложение или внешнюю информацию, необходимую для проверки, программное обеспечение должно сделать определенные предположения относительно отсутствующего кода или внешней информации.
Например, если вы не предоставляете main , программное обеспечение генерирует main который вызывает только незакрытые функции. Если func1 требования func2, сгенерированный main не звонит func2 снова. Проверка проверяет наличие ошибок во время выполнения в func2 только из контекста вызова в func1.
Предположения таковы, что они применимы к большинству приложений. Однако в некоторых случаях предположения по умолчанию могут не дать точного описания среды выполнения. Если предположения не являются ожидаемыми, результаты проверки могут быть неожиданными.
Проверьте, можно ли отследить результат проверки по предположению программного обеспечения. Неполный список допущений см. в разделе Допущения анализа проверочных кодов. Дополнительный перечень допущений приведен в codeprover_limitations.pdf в polyspaceroot\polyspace\verifier\code_prover_desktop
Часто можно изменить предположения по умолчанию, используя определенные опции.
Target and Compiler: Проверьте, нужно ли задать параметр для эмуляции поведения компилятора.
Например, если вы хотите, чтобы частные операций деления округлялись вниз, а не вверх, используйте опцию Division round down (-div-round-down).
Входы и упрямство: Посмотрите, если вы должны внешне ограничить некоторые переменные.
Например, если необходимо ограничить глобальную переменную в определенном диапазоне, используйте опцию Constraint setup (-data-range-specifications).
Многозадачность: Посмотрите, забыли ли вы указать некоторые задачи или механизмы защиты.
Например, если необходимо указать, что функция представляет собой неразрушаемое прерывание, используйте опцию Interrupts (-interrupts).
Проверка подтверждения кода: при проверке модуля без 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.