#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);
}