Code Prover Assumptions About Stubbed Functions

The verification stubs functions that are not defined in your source code or that you choose to stub. For a stubbed function:

The verification makes certain assumptions about the function return value and other side effects of the function.
You can fine-tune the assumptions by specifying constraints.
The verification ignores the function body if it exists. Operations in the function body are not checked for run-time errors.

If the verification of a function body is imprecise and causes many orange checks when you call the function, you can choose to stub the function. To reduce the number of orange checks, you stub the function, and then constrain the return value of the function and specify other side effects.

To stub functions, you can use these options:

Functions to stub (-functions-to-stub): Specify functions that you want stubbed.
Generate stubs for Embedded Coder lookup tables (-stub-embedded-coder-lookup-table-functions): Stub functions that contain lookup tables in code generated from models using Embedded Coder^®.
-code-behavior-specifications: Stub functions that correspond to a standard function that Polyspace^® recognizes.

If you use the first option to stub a function, you constrain the function return value and model other side effects by specifying constraints. If you want to specify constraints more fine-grained than the ones available through the Polyspace constraint specification interface, define your own stubs. If you use the other options to stub functions, the software itself constrains the function return value and models its side effects appropriately. For more information on specifying constraints, see:

The verification makes the following assumptions about the arguments of stubbed functions.

Function Return Value

Assumptions

The verification assumes that:

The variable returned by the function takes the full range of values allowed by its data type.
If the function returns an enum variable, the variable value is in the range of the enum. For instance, if an enum type takes values {0,5,-1,32} and a stubbed function has that return type, the verification assumes that the function returns values in the range -1..32.
If the function returns a pointer, the pointer is not NULL and safe to dereference. The pointer does not point to dynamically allocated memory or another variable in your code.
(C++ only) The operator new returns allocated memory. Operators such as operator=, operator+=, operator--(prefixed version) or operator<< returns:
- A reference to *this, if the operator is part of a class definition.
  For instance, if an operator is defined as:
```
class X {
  X& operator=(const X& arg) ;
};
```
  It returns a reference to *this (the object that calls the operator). The object that calls the operator or its data members have the full range of values allowed by their type.
- The first argument, if the operator is not part of a class definition.
  For instance, if an operator is defined as:
```
X& operator+=(X& arg1, const X& arg2) ;
```
  It returns arg1. The object that arg1 refers to or its data members have the full range of values allowed by their type.
(C++ only) Functions declared with __declspec(no_return) (Visual Studio^®) or __attribute__ ((noreturn)) (GCC) do not return. If your code contains such a function, you can see a dashed red underline on the function call along with a tooltip. For instance, in this example, you see a dashed red underline on the call to fatal():
```
void fatal(int) __attribute__ ((noreturn));
          
void main() {
    int x = 0;
    fatal(x);
    x++;
}
```

How to Change Assumptions

You can change the default assumptions about the function return value.

If the function returns a non-pointer variable, you can constrain its range. Use the option Constraint setup (-data-range-specifications).
Through the constraint specification interface, you can specify an absolute range [min..max]. To specify more complicated constraints, write a function stub.
For instance, an undefined function has the prototype:
```
int func(int ll, int ul);
```
Suppose you know that the function return value lies between the first and the second arguments. However, the software assumes full range for the return value because the function is not defined. To model the behavior that you want and reduce orange checks from the imprecision, write a function stub as follows:
```
int func(int ll, int ul) {
     int ret;
     assert(ret>=ll && ret <=ul);
     return ret;
}
```
Provide the function stub in a separate file for verification. The verification uses your stub as the function definition.
If the definition of func exists in your code and you want to override the definition because the verification of the function body is imprecise, embed the actual definition and the stub in a #ifdef statement:
```
#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
```
Define the macro POLYSPACE by using the option Preprocessor definitions (-D). The verification uses your stub instead of the actual function definition.
If the function returns a pointer variable, you can specify that the pointer might be NULL.
- To specify this assumption for all stubbed functions, use the option Consider environment pointers as unsafe (-stubbed-pointers-are-unsafe).
- To specify this assumption for specific stubbed functions, use the option Constraint setup (-data-range-specifications).

Function Arguments That are Pointers

Assumptions

The verification assumes that:

If the argument is a pointer, the function can write any value to the object that the pointer points to. The range of values is constrained by the argument data type alone.
For instance, in this example, the verification assumes that the stubbed function stubbedFunc writes any possible value to val. Therefore, the assertion is orange.
```
void stubbedFunc(int*);

void main() {
    int val=0, *ptr=&val;
    stubbedFunc(ptr);
    assert(val==0);
}
```
If the argument is a pointer to a structure, the function can write any value to the structure fields. The range of values is constrained only by the data type of the fields.
In C++ code, only first level data members of a structure can be written via a pointer to the structure. For instance, in this example, the analysis has knowledge of what pb->j points to, but not what pb->pa->i points to. So, after the call to Foo, b.j appears as initialized but a.i is not initialized.
```
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;
}
```
If the argument is a pointer to another pointer, the function can write any value to the object that the second pointer points to (C code only). This assumption continues to arbitrary depths of a pointer hierarchy.
For instance, suppose that a pointer **pp points to another pointer *p, which points to an int variable var. If a stubbed function takes **p as argument, the verification assumes that following the function call, var has any int value. *p can point to anywhere in allocated memory or can point to var but does not point to another variable in the code.
If the argument is a function pointer, the function that it points to gets called (C code only).
For instance, in this example, the stubbed function stubbedFunc takes a function pointer funcPtr as argument. funcPtr points to func, which gets called when you call stubbedFunc.
```
typedef int (*typeFuncPtr) (int);

int func(int x){
  	return x;
}

int stubbedFunc(typeFuncPtr);

void main() {
    typeFuncPtr funcPtr = (typeFuncPtr)(&func);
    int result = stubbedFunc(funcPtr);
}
```
If the function pointer takes another function pointer as argument, the function that the second function pointer points to gets stubbed.

How to Change Assumptions

You can constrain the range of the argument that is passed by reference. Use the option Constraint setup (-data-range-specifications).

Through the constraint specification interface, you can specify an absolute range [min..max]. To specify more complicated constraints, write a function stub.

For instance, an undefined function has the prototype:

void func(int *x, int ll, int ul);

Suppose you know that the value written to x lies between the second and the third arguments. However, the software assumes full range for the value of *x because the function is not defined. To model the behavior that you want and reduce orange checks from the imprecision, write a function stub as follows:

void func(int *x, int ll, int ul) {
     assert(*x>=ll && *x <=ul);
}

Provide the function stub in a separate file for verification. The verification uses your stub as the function definition.

If the definition of func exists in your code and you want to override the definition because the verification of the function body is imprecise, embed the actual definition and the stub in a #ifdef statement:

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

Define the macro POLYSPACE by using the option Preprocessor definitions (-D). The verification uses your stub instead of the actual function definition.

Global Variables

Assumptions

The verification assumes that the function stub does not modify global variables.

How to Change Assumptions

To model write operations on a global variable, write a function stub.

For instance, an undefined function has the prototype:

void func(void);

Suppose you know that the function writes the value 0 or 1 to a global variable glob. To model the behavior that you want, write a function stub as follows:

void func(void) {
     volatile int randomVal;
     if(randomVal)
          glob = 0;
     else
          glob = 1;
}

Provide the function stub in a separate file for verification. The verification uses your stub as the function definition.

#ifdef POLYSPACE
void func(void) {
     volatile int randomVal;
     if(randomVal)
          glob = 0;
     else
          glob = 1;
}
#else
void func(void) {
     /* Your function body */
}
#endif

Define the macro POLYSPACE using the option Preprocessor definitions (-D). The verification uses your stub instead of the actual function definition.