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
User interface (desktop products only): In your project configuration, the option is on the Code Prover Verification node. See Dependencies for other options that you must also enable.
User interface (Polyspace Platform, desktop products only): In your project configuration, the option is on the Static Analysis tab on the Run Time Errors node.
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; }
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
orchar
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 keywordsstatic
andconst
.all
The generated
main
initializes all global variables except those declared with keywordconst
.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 following are true:
Your code does not contain a
main
function.Verify module or library (-main-generator)
is selected.
The option is disabled if 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= |
Default:
public |
Example (Code Prover): polyspace-code-prover
-sources |
Example (Code Prover
Server):
polyspace-code-prover-server -sources
|
Version History
See Also
Verify module or library (-main-generator)
Topics
- Specify Polyspace Analysis Options
- Verify C Application Without main Function (Polyspace Code Prover)