Correctness condition

Несоответствие происходит во время броска указателя или использования указателя функции

расширьте все на странице

Описание

Эта проверка определяет ли:

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

Диагностирование этой проверки

Рассмотрите и зафиксируйте проверки условия правильности

Примеры

развернуть все

Массив сопоставлен с большим массивом

typedef int smallArray[10];
typedef int largeArray[100];


void main(void) {
    largeArray myLargeArray;
    smallArray *smallArrayPtr = (smallArray*) &myLargeArray;
    largeArray *largeArrayPtr = (largeArray*) smallArrayPtr;
}

В этом примере:

В первом слепке указателя, указателе типа largeArray брошен к указателю типа smallArray. Поскольку тип данных smallArray представляет меньший массив, проверка Correctness condition является зеленой.
Во втором слепке указателя, указателе типа smallArray брошен к указателю типа largeArray. Поскольку тип данных largeArray представляет больший массив, проверка Correctness condition является красной.

Указатель функции не указывает на функцию

typedef void (*callBack) (float data);
typedef struct {
    char funcName[20];
    callBack func;
} funcStruct;

funcStruct myFuncStruct;

void main(void) {
    float val = 0.f;
    myFuncStruct.func(val);
}

В этом примере, глобальная переменная myFuncStruct не инициализируется, таким образом, указатель функции myFuncStruct.func содержит NULL. Когда указатель myFuncStruct.func разыменовывается, проверка Correctness condition производит красную ошибку.

Указатель функции указывает, чтобы функционировать посредством абсолютного использования адреса

#define MAX_MEMSEG 32764
typedef void (*ptrFunc)(int memseg);
ptrFunc operation = (ptrFunc)(0x003c);

void main(void) {
    for (int i=1; i <= MAX_MEMSEG; i++)
        operation(i);
}

В этом примере, указатель функции operation брошен к содержимому ячейки памяти. Polyspace^® не может определить, содержит ли местоположение переменную или функциональный код и хорошо ли вводится функция. Поэтому, когда указатель operation разыменовывается и используется в вызове функции, проверка Correctness condition является оранжевой.

После оранжевой проверки Correctness condition из-за абсолютного использования адреса, программное обеспечение принимает, что следующие переменные имеют полный спектр значений, позволенных их типом:

Переменная, хранящая возвращаемое значение от вызова функции.
В следующем примере программное обеспечение принимает что возвращаемое значение operation полный диапазон.
```
typedef int (*ptrFunc)(int);
ptrFunc operation = (ptrFunc)(0x003c);

int main(void) {
  return operation(0);
}
```
Переменные, которые могут быть изменены через аргументы функции.
В следующем примере, указатель функции operation берет аргумент ptr указателя это указывает на переменную var. После вызова operation, программное обеспечение принимает тот var имеет полнофункциональное значение.
```
typedef void (*ptrFunc)(int*);
ptrFunc operation = (ptrFunc)(0x003c);

void main(void) {
  int var;
  int *ptr=&var;
  operation(ptr);
}
```

Указатель функции указывает, чтобы функционировать с неправильным типом аргумента

typedef struct {
  double real;
  double imag;
} complex;

typedef int (*typeFuncPtr) (complex*);

int func(int* x);

void main() {
  typeFuncPtr funcPtr = (typeFuncPtr)&func;
  int arg = 0, result = funcPtr((complex*)&arg);
}

В этом примере, указатель функции funcPtr точки к функции с типом аргумента complex*. Однако указатель присвоен адрес функционального func чьим типом аргумента является int*. Из-за этого несоответствия типов проверка Correctness condition является оранжевой.

Указатель функции указывает, чтобы функционировать с неправильным количеством аргументов

typedef int (*typeFuncPtr) (int, int);

int func(int);

void main() {
    typeFuncPtr funcPtr = (typeFuncPtr)&func;
    int arg1 = 0, arg2 = 0, result = funcPtr(arg1,arg2);
}

В этом примере, указатель функции funcPtr точки к функции с двумя int аргументы. Однако это присвоено функциональный func который имеет один int аргумент только. Из-за этого несоответствия в количестве аргументов проверка Correctness condition является оранжевой.

Указатель функции указывает, чтобы функционировать с неправильным типом возврата

typedef double (*typeFuncPtr) (int);

int func(int);

void main() {
    typeFuncPtr funcPtr = (typeFuncPtr)&func;
    int arg = 0;
    double result = funcPtr(arg);
}

В этом примере, указатель функции funcPtr точки к функции с возвратом вводят double. Однако это присвоено функциональный func чей возвращаются, типом является int. Из-за этого несоответствия в ответ вводит, проверка Correctness condition является оранжевой.

Переменная выходит за пределы Глобальной переменной, Утверждают область значений

int glob = 0;
int func();

void main() {
    glob = 5;
    glob = func();
    glob+= 20;
}

В этом примере, области значений 0..10 был задан для глобальной переменной glob.

В операторе glob=5;, зеленая проверка Correctness condition появляется на glob.
В операторе glob=func();, оранжевая проверка Correctness condition появляется на glob потому что возвращаемое значение заблокированного функционального func может найтись вне 0..10.
После этого оператора Polyspace рассматривает тот glob имеет значения в 0..10.
В операторе glob+=20;, красная проверка Correctness condition появляется на glob потому что после сложения, glob имеет значения в 20..30.

См. также Ограничивают Область значений Глобальной переменной.

Проверяйте информацию

Группа: Другой

Язык: C | C++

Акроним: COR

Темы

Документация Polyspace Code Prover

Поддержка

Сообщество Экспонента

Документация