Выполните один или несколько из этих шагов, пока вы не определите фиксацию для проверки Correctness condition. Существует несколько способов зафиксировать красную или оранжевую проверку. Для описания проверки и примеров кода, смотрите Correctness condition.
Иногда, специально для оранжевой проверки, можно решить, что проверка не представляет действительную ошибку, но предположение Polyspace®, которое не верно для кода. Если можно использовать аналитическую опцию, чтобы ослабить предположение, повторно выполнить верификацию с помощью той опции. В противном случае можно добавить комментарий и выравнивание в результате или коде.
Для общего рабочего процесса, который применяется ко всем проверкам, смотрите, Интерпретируют Результаты Polyspace Code Prover.
На панели Results List выберите проверку. Просмотрите причину, проверяют панель Result Details. Следующий список показывает некоторые возможные причины:
Массив преобразован в другой массив большего размера.
В следующем примере происходит красная проверка, потому что массив преобразован в другой массив большего размера.
Когда разыменовано, указатель функции имеет значение NULL.
В следующем примере происходит красная проверка, потому что, когда разыменовано, указатель функции имеет значение NULL.
Когда разыменовано, указатель функции не указывает на функцию.
В следующем примере происходит оранжевая проверка, потому что Polyspace не может определить, указывает ли указатель функции на функцию, когда разыменовано. Эта ситуация может произойти, если, например, вы присваиваете абсолютный адрес указателю функции.
Указатель функции указывает на функцию, но типы аргумента указателя и функции не соответствуют. Например:
typedef int (*typeFuncPtr) (complex*); int func(int* x); . . typeFuncPtr funcPtr = &func;
В следующем примере красная проверка происходит потому что:
Указатель функции указывает на функциональный func.
func ожидает аргумент типа int, но соответствующий аргумент указателя функции является структурой.
Указатель функции указывает на функцию, но количества аргумента указателя и функции не соответствуют. Например:
typedef int (*typeFuncPtr) (int, int); int func(int); . . typeFuncPtr funcPtr = &func;.
В следующем примере красная проверка происходит потому что:
Указатель функции указывает на функциональный func.
func ожидает один аргумент, но указатель функции имеет два аргумента.
Указатель функции указывает на функцию, но типы возврата указателя и функции не соответствуют. Например:
typedef double (*typeFuncPtr) (int); int func(int); . . typeFuncPtr funcPtr = &func;
В следующем примере красная проверка происходит потому что:
Указатель функции указывает на функциональный func.
func возвращает int значением, но типом возврата указателя функции является double.
Значение переменной выходит за пределы диапазона, который вы указываете через режим Global Assert. Смотрите Ограничивают Область значений Глобальной переменной.
В следующем примере красная проверка происходит потому что:
Вы указываете диапазон 0... 10 для переменной glob.
Значение переменной выходит за пределы этой области значений.
На основе информации о проверке о панели Result Details выполните дальнейшие шаги, чтобы определить первопричину. Можно выполнить следующие шаги в пользовательском интерфейсе Polyspace только.
| Проверяйте информацию | Как определить первопричину |
|---|---|
Массив преобразован в другой массив большего размера. |
|
Проблемы при разыменовании указателя функции:
|
|
Значение переменной выходит за пределы диапазона, который вы указываете через режим Global Assert. | Просмотрите все предыдущие экземпляры глобальной переменной. Идентифицируйте подходящую точку, чтобы ограничить переменную.
|
Смотрите, можно ли проследить оранжевую проверку до предположения Polyspace, которое происходит ранее в коде. Если предположение не сохраняется в вашем случае, добавьте комментарий или выравнивание в вашем результате или коде. Смотрите Результаты Polyspace Адреса Через Исправления ошибок или Выравнивания.
