Ignore default initialization of global variables (-no-def-init-glob)

Consider global variables as uninitialized unless explicitly initialized in code

Description

This option applies to Code Prover only. It does not affect a Bug Finder analysis.

Specify that Polyspace^® must not consider global and static variables as initialized unless they are explicitly initialized in the code.

Set Option

User interface (desktop products only): In your project configuration, the option is on the Inputs & Stubbing node.

Command line and options file: Use the option -no-def-init-glob. See Command-Line Information.

Why Use This Option

The C99 Standard specifies that global variables are implicitly initialized. The default analysis follows the Standard and considers this implicit initialization.

If you want to initialize specific global variables explicitly, use this option to find the instances where global variables are not explicitly initialized.

Settings

On

Polyspace ignores implicit initialization of global and static variables. The verification generates a red Non-initialized variable error if your code reads a global or static variable before writing to it.

If you enable this option, global variables are considered uninitialized unless you explicitly initialize them in the code. Note that this option overrides the option Variables to initialize (-main-generator-writes-variables) (Polyspace Code Prover). Even if you initialize variables with the generated main, this option forces the analysis to ignore the initialization.

Off (default)

Polyspace considers global variables and static variables to be initialized according to C99 or ISO^® C++ standards. For instance, the default values are:

• 0 for int

• 0 for char

• 0.0 for float

Tips

Static local variables have the same lifetime as global variables even though their visibility is limited to the function where they are defined. Therefore, the option applies to static local variables.

Command-Line Information

Parameter: -no-def-init-glob

Default: Off

Example (Code Prover): polyspace-code-prover -sources file_name -no-def-init-glob

Example (Code Prover Server): polyspace-code-prover-server -sources file_name -no-def-init-glob