Main Content

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

Check that global variables are assigned values in designed initialization code

Since R2020a

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.

The initialization code depends on the source code you verify:

  • When verifying whole application — The initialization code starts from the beginning of the main() function and continues up to this #pragma directive:

    #pragma polyspace_end_of_init
    You cannot specify this #pragma more than once. Since compilers ignore unrecognized pragmas, the presence of this pragma does not affect program execution.

  • When verifying modules or libraries — The initialization code is the sequence of functions called before the generated main. Specify these function by using the option Initialization functions (-functions-called-before-main). Polyspace assumes that the initialization functions are called in the same sequence in which they are specified.

Set Option

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

User interface (Polyspace Platform, desktop products only): In your project configuration, the option is on the Static Analysis tab on the Run Time Errors > 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 block starting symbol (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 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

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.

  • When using this check, best practice is to specify the initialization code correctly. For example:

    • Specify the initialization code such that all initializations of global variables are covered. That is, place the directive #pragma polyspace_end_of_init after the end of the initialization. Alternatively, when verifying modules, specify all functions that perform initialization. Otherwise, Polyspace can flag a variable that is initialized outside the marked initialization code as uninitialized.

    • Avoid placing the directive #pragma polyspace_end_of_init in a block. If you place the pragma in a block, the paths that do not end in the block is excluded from this check.

      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 directive #pragma polyspace_end_of_init 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

Version History

Introduced in R2020a

expand all

See Also

| | |

Topics