Variables to initialize (-main-generator-writes-variables)

Specify global variables that you want the generated main to initialize

Description

This option affects a Code Prover analysis only.

This option is not available for code generated from MATLAB^® code or Simulink^® models.

Specify global variables that you want the generated main to initialize. Polyspace^® considers these variables to have any value allowed by their type.

Set Option

Set the option using one of these methods:

• Polyspace user interface (desktop products only): In your project configuration, select the Code Prover Verification node and then select a value for this option.

• Polyspace Platform user interface (desktop products only): In your project configuration, on the Static Analysis tab, select the Run Time Errors node and then select a value for this option. See Dependencies for other options you must enable first.

• Command line and options file: Use the option -main-generator-writes-variables. See Command-Line Information.

Why Use This Option

If you are verifying a module or library, Code Prover generates a main function if one does not exist. If a main exists, the analysis uses the existing main.

A Code Prover analysis of a module without a main function makes some default assumptions about global variable initialization. The analysis assumes that global variables that are not explicitly initialized can have the full range of values allowed by their data types upon each entry into an uncalled function. For instance, in the example below, which does not have a main function, the variable glob is assumed to have all possible int values both in foo and bar (despite the modification in foo). The assumption is a conservative one since the call context of foo and bar, including which function gets called earlier, is not known.

int glob;

int foo() {
   int locFoo = glob;
   glob++;
   return locFoo;
}

int bar() {
   int locBar = glob;
   return locBar;
}

To implement this assumption, the generation main initializes such global variables to full-range values before calling each otherwise uncalled function. Use this option to modify this default assumption and implement a different initialization strategy for global variables.

Settings

Default: public

uninit

The generated main only initializes global variables that you have not initialized during declaration.

none

The generated main does not initialize global variables.

Global variables are initialized according to the C/C+ standard. For instance, int or char variables are initialized to 0, float variables to 0.0, and so on.

public

The generated main initializes all global variables except those declared with keywords static and const.

all

The generated main initializes all global variables except those declared with keyword const.

custom

The generated main only initializes global variables that you specify. Click to add a field. Enter a global variable name.

Dependencies

You can use this option only if the option Verify module or library (-main-generator) (Polyspace Code Prover) is selected.

The option is ignored if:

• Your code contains a main function.

• You enable the option Ignore default initialization of global variables (-no-def-init-glob). Global variables are considered as uninitialized until you explicitly initialize them in the code.

Tips

This option only affects global variables that are defined in the project. If a global variable is declared as extern, the analysis considers that the variable can have any value allowed by its data type, irrespective of the value of this option.

Command-Line Information

Parameter: -main-generator-writes-variables

Value: uninit | none | public | all | custom=variable1[,variable2[,...]]

Default: public

Example (Code Prover): polyspace-code-prover -sources file_name -main-generator -main-generator-writes-variables all

Example (Code Prover Server): polyspace-code-prover-server -sources file_name -main-generator -main-generator-writes-variables all

Version History

R2024a: Option -main-generator-writes-variables supports uninit mode in C

Starting in R2024a, the option -main-generator-writes-variables supports the value uninit for a Code Prover analysis where the source code language is set to C. Previously, the value uninit was supported only if the language was CPP or C-CPP.

R2024a: Option -main-generator-writes-variables defaults to public mode in C++

Starting in R2024a, the option -main-generator-writes-variables defaults to public for a Code Prover analysis irrespective of the source code language.

The previous default value was:

• public if the project language was set to C.

• uninit if the project language was set to CPP or C-CPP.