Check that global variables are initialized after warm reboot (-check-globals-init)

Check that global variables are assigned values in designed initialization code

Description

This option affects a Code Prover analysis only.

Specify that Polyspace® must check whether all non-const global variables (and local static variables) are explicitly initialized at declaration or within a section of code marked as initialization code.

To indicate the end of initialization code, you enter the line

#pragma polyspace_end_of_init
in the main function (only once). The initialization code starts from the beginning of main and continues up to this pragma.

Since compilers ignore unrecognized pragmas, the presence of this pragma does not affect program execution.

Set Option

User interface (desktop products only): In your project configuration, the option is on the Check Behavior node.

Command line and options file: Use the option -check-globals-init. See Command-Line Information.

Why Use This Option

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 use this option to delimit the initialization code and verify that all non-const global variables are indeed initialized in a warm reboot.

For instance, in this simple example, the global variable aVar is initialized in the initialization code section but the variable anotherVar is not.

int aVar;
const int aConst = -1;
int anotherVar;

int main() {
      aVar = aConst;
#pragma polyspace_end_of_init
      return 0;
}

Settings

On

Polyspace checks whether all global variables are initialized in the designated initialization code. The initialization code starts from the beginning from main and continues up to the pragma polyspace_end_of_init.

The results are reported using the check Global variable not assigned a value in initialization code.

Off (default)

Polyspace does not check for initialization of global variables in a designated code section.

However, the verification continues to check if a variable is initialized at the time of use. The results are reported using the check Non-initialized variable.

Dependencies

You can use this option and designate a section of code as initialization code only if:

Note that the pragma must appear only once in the main function. The pragma can appear before or after variable declarations but must appear after type definitions (typedef-s).

You cannot use this option with the following options:

Tips

  • You can use this option along with the option Verify initialization section of code only (-init-only-mode) to check the initialization code before checking the remaining program.

    This approach has the following benefits compared to checking the entire code in one run:

    • Run-time errors in the initialization code can invalidate analysis of the remaining code. You can run a comparatively quicker check on the initialization code before checking the remaining program.

    • You can review results of the checker Global variable not assigned a value in initialization code relatively easily.

      Consider this example. There is an orange check on var because var might remain uninitialized when the if and else if statements are skipped.

      int var;
 
int checkSomething(void);
int checkSomethingElse(void);
 
int main() {
    int local_var;
    if(checkSomething())
    {
        var=0;
    }
    else if(checkSomethingElse()) {
        var=1;
    }
    #pragma polyspace_end_of_init
    var=2;
    local_var = var;
    return 0;
}

      To review this check and understand when x might be non-initialized, you have to browse through all instances of x on the Variable Access pane. If you check the initialization code alone, only the code in bold gets checked and you have to browse through only the instances in the initialization code.

  • The check is only as good as your placement of the pragma polyspace_end_of_init. For instance:

    • Place the pragma only after initialization code ends.

      Otherwise, a variable might appear falsely uninitialized.

    • Try to place the pragma directly in the main function, that is, outside a block. If you place the pragma in a block, the check considers only those paths that end in the block.

      All paths that end in the block might have a variable initialized but paths that skip the block might let the variable go uninitialized. If you do place the pragma in a block, make sure that it is okay if a variable stays uninitialized outside the block.

      For instance, in this example, the variable var is initialized on all paths that end at the location of the pragma. The check is green despite the fact that the if block might be skipped, letting the variable go uninitialized.

      int var;

int func();

int main() {
    int err = func();
    if(err) {
        var = 0;
 #pragma polyspace_end_of_init
    }
    int a = var;   
    return 0;
}

      The issue is detected by the checker if you place the pragma after the if block ends.

    • Do not place the pragma in a loop.

      If you place the pragma in a loop, you can see results that are difficult to interpret. For instance, in this example, both aVar and anotherVar are initialized in one iteration of the loop. However, the pragma only considers the first iteration of the loop when it shows a green check for initialization. If a variable is initialized on a later iteration, the check is orange.

      int aVar;
int anotherVar;

void main() {
    for(int i=0; i<=1; i++) {
        if(i == 0)
            aVar = 0;
        else
            anotherVar = 0;
        #pragma polyspace_end_of_init
    }
}
      The check is red if you verify initialization code alone and do not initialize a variable in the first loop iteration. To avoid these incorrect red or orange checks, do not place the pragma in a loop.

    • To determine the initialization of a structure, a regular Code Prover analysis only considers fields that are used.

      If you check initialization code only using the option Verify initialization section of code only (-init-only-mode), the analysis covers only a portion of the code and cannot determine if a variable is used beyond this portion. Therefore, the checks for initialization consider all structure fields, whether used or not.

Command-Line Information

Parameter: -check-globals-init
Default: Off
Example (Code Prover): polyspace-code-prover -sources file_name -check-globals-init
Example (Code Prover Server): polyspace-code-prover-server -sources file_name -check-globals-init

See Also

|

Topics

Introduced in R2020a

Polyspace Code Prover Documentation

Support