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

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

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

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

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

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

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

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

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

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

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

В коде C++ только элементы данных первого уровня структуры могут быть записаны через указатель на структуру. Например, в этом примере анализ обладает знаниями о том, что 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;
}

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

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

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

Например, в этом примере функция упора 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);
}