Code Prover Assumptions About Global Variable Initialization

Global variables are variables that are visible throughout the program (unless shadowed by local variables). A Code Prover analysis makes specific assumptions about the initialization of global variables.

Global Variable Initialization When `main` Function Exists

If your code contains a main function, a Code Prover verification considers that global variables are initialized according to ANSI^® C standards. The default values are:

0 for int
0 for char
0.0 for float

and so on.

Sometimes, you might want to check if global variables are explicitly initialized in the code. For instance:

In a warm reboot, to save time, the bss segment of a program, which might hold variable values from a previous state, is not loaded. Instead, the program is supposed to explicitly initialize all non-const variables without default values before execution. You can delimit this initialization code and verify that all non-const global variables are indeed initialized in a warm reboot.
To delimit a section of code as initialization code, enter the pragma polyspace_end_of_init in the main function. The initialization code begins from the main function and continues up to this pragma. Use these options to check the initialization code only and determine whether all global variables are initialized in this section of the code:
- Check that global variables are initialized after warm reboot (-check-globals-init)
- Verify initialization section of code only (-init-only-mode)
The Code Prover analysis reports non-initialized variables using red or orange results in the initialization code for the checks:
- Global variable not assigned a value in initialization code
- Non-initialized variable
To only check if global variables are explicitly initialized at the point of use, use the option Ignore default initialization of global variables (-no-def-init-glob).
The Code Prover analysis reports non-initialized variables using red or orange results for the check Non-initialized variable.

Global Variable Initialization When `main` Function Does Not Exist

If your code does not have a main function, Code Prover begins verifying each uncalled function with the assumption that global variables have full range value, constrained only by their data type. See also Code Prover Assumptions About Variable Ranges From Data Types.

For instance, consider this example:

int glob;
void func1_callee();

void func1() {
    int loc =  glob;
    if(!glob)
       func1_callee();
}

void func1_callee() {
    int loc = glob;
}

void func2() {
    int loc = glob;
}

In both func1 and func2, the global variable glob and consequently the local variable loc has full range of int values.

However, only uncalled functions begin with full-range values of global variables. The function func1_callee is called in func1 after the value of glob is constrained to zero. In func1_callee, the global variable glob and consequently the local variable loc has the constrained value zero.

How Code Prover Implements Assumption About Global Variable Initialization

The software uses the dummy function _init_globals() to initialize global variables. The _init_globals() function is the first function implicitly called in the main function (or generated main function if there is no main).

Consider the following code in the application gv_example.c.

extern int func(int);

int garray[3] = {1, 2, 3};  
int gvar = 12;

int main(void) {
    int i, lvar = 0;
    for (i = 0; i < 3; i++) 
       lvar += func(garray[i] + gvar);
    return lvar;
}

After verification:

On the Results List pane, if you select File from the list, under the node gv_example.c, you see _init_globals.
On the Variable Access pane, gv_example._init_globals represents the initialization of the global variable. The Values column shows the value of the global variable immediately after initialization.

What Initialization Means for Complex Data Types

The following table lists what is checked for each data type to determine initialization. The check happens at the time of read operations for the check Non-initialized variable and at the end of the initialization section for the check Global variable not assigned a value in initialization code.

Data Type	What Green Check for Initialization Means
Fundamental types (`int`, `double`, etc.)	The variable is written at least once.
Array data types	Every array element is written at least once.
Structured data types	Every structure field that is used is written at least once. If you check initialization code only using the option `Verify initialization section of code only (-init-only-mode)`, the analysis checks for initialization of all structure fields, whether used or not. In the special case where none of the fields are used, the checks for initialization are orange instead of green if all the fields.are uninitialized.
Pointers	The pointer is written at least once. However, Code Prover does not check for initialization of the pointed buffer (till you dereference the pointer).
Enumerations	The `enum` variable is written at least once. However, Code Prover does not check if the variable has one of the `enum` values.