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

Переменная, возвращенная функцией, берет полный спектр значений, позволенных его типом данных.

Если функция возвращает enum переменная, значение переменных находится в области значений перечисления. Например, если enum тип принимает, значения {0,5,-1,32} и заблокированная функция имеют тот тип возврата, верификация принимает, что функция возвращает значения в области значений-1.. 32.

Если функция возвращает указатель, указатель не является ПУСТЫМ и безопасным разыменовать. Указатель не указывает на динамически выделенную память или другую переменную в вашем коде.

C++ определенные предположения: оператор new возвращает выделенную память. Операторы, такие как operator=оператор + =оператор--(снабженная префиксом версия) или operator<< возвращается:

Функции объявляются с __declspec(no_return) (Визуальный Studio^®) или __attribute__ ((noreturn)) (GCC) не возвращаются.

Если функция возвращает неуказательную переменную, можно ограничить ее область значений. Используйте опцию Constraint setup (-data-range-specifications).

Через ограничительный интерфейс спецификации можно указать абсолютный диапазон [minMax ]. Чтобы задать более сложные ограничения, запишите функциональный тупик.

Например, неопределенная функция имеет прототип:

int func(int ll, int ul);

int func(int ll, int ul) {
     int ret;
     assert(ret>=ll && ret <=ul);
     return ret;
}

Если определение func существует в вашем коде, и вы хотите заменить определение, потому что верификация тела функции неточна, встройте фактическое определение и тупик в #ifdef оператор:

#ifdef POLYSPACE
int func(int ll, int ul) {
     int ret;
     assert(ret>=ll && ret <=ul);
     return ret;
}
#else
int func(int ll, int ul) {
    /*Your function body */ 
}
#endif

Если функция возвращает переменную указателя, можно указать, что указателем может быть NULL.

Если аргумент является указателем, функция может записать любое значение в объект, на который указывает указатель. Область значений значений ограничивается одним только типом данных аргумента.

Например, в этом примере, верификация принимает что заблокированный функциональный stubbedFunc записи любое возможное значение к val. Поэтому утверждение является оранжевым.

void stubbedFunc(int*);

void main() {
    int val=0, *ptr=&val;
    stubbedFunc(ptr);
    assert(val==0);
}

Если аргумент является указателем на структуру, функция может записать любое значение в поля структуры. Область значений значений ограничивается только по условию тип полей.

В Коде С++ только первые элементы данных уровня структуры могут быть записаны через указатель на структуру. Например, в этом примере, анализ имеет знание какой pb->j точки к, но не, что pb->pa->i точки к. Так, после вызова Foo, b.j появляется, как инициализировано, но a.i не инициализируется.

struct A {
   int i;
};
 
struct B {
   A* pa;
   int j;
};
 
void Foo(B*);
 
void main() {
    A a;
    B b;
    b.pa = &a;
    Foo(&b); 
    int var1 = b.j;
    int var2 = a.i;
}

Если аргумент является указателем на другой указатель, функция может записать любое значение в объект, который второй указатель указывает на (Только код С). Это предположение продолжается к произвольным глубинам иерархии указателя.

Например, предположите что указатель **pp точки к другому указателю *p, который указывает на int переменная var. Если заблокированная функция берет **p в качестве аргумента верификация принимает что, следуя за вызовом функции, var имеет любой int значение. *p может указать на где угодно в выделенной памяти или может указать на var но не указывает на другую переменную в коде.

Если аргумент является указателем функции, функция, на которую он указывает, вызвана (Только код С).

Например, в этом примере, заблокированном функциональном stubbedFunc берет указатель функции funcPtr в качестве аргумента. funcPtr точки к func, который называется, когда вы вызываете stubbedFunc.

typedef int (*typeFuncPtr) (int);

int func(int x){
  	return x;
}

int stubbedFunc(typeFuncPtr);

void main() {
    typeFuncPtr funcPtr = (typeFuncPtr)(&func);
    int result = stubbedFunc(funcPtr);
}