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