Выполните один или несколько из следующих шагов до тех пор, пока вы не определите исправление для проверки Correctness condition. Существует несколько способов исправить красный или оранжевый чек. Для получения описания примеров проверки и кода смотрите Correctness condition.
Иногда, особенно для оранжевого чека, можно определить, что чек представляет не реальную ошибку, а Polyspace® предположение, что не соответствует действительности для вашего кода. Если для ослабления допущения можно использовать опцию анализа, повторите верификацию с помощью этой опции. В противном случае можно добавить комментарий и обоснование в результат или код.
Общий рабочий процесс, который применяется ко всем проверкам, см. в разделе Интерпретация результатов Prover кода в пользовательском интерфейсе рабочего стола Polyspace.
На панели Results List выберите проверку. Проверьте причину проверки на панели Result Details. В следующем списке показаны некоторые возможные причины:
Массив преобразуется в другой массив большего размера.
В следующем примере проверка красного цвета происходит, потому что массив преобразуется в другой массив большего размера.
При размене указатель на функцию имеет значение NULL.
В следующем примере красная проверка происходит, потому что, когда dereferenced, указатель на функцию имеет значение 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, которое происходит ранее в коде. Если предположение не имеет значения true в вашем случае, добавьте комментарий или обоснование в свой результат или код. Смотрите Адрес Результаты Polyspace через исправления ошибок или обоснования.
