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 Add row to table icon. 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) is selected.

The option is ignored if:

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

expand all

See Also

Topics