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


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

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

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 dereferenced, проверка 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 dereferenced и используется в вызове функции, проверка Correctness condition оранжевая.

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

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.

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