Verify module or library (-main-generator)

Generate a main function if source files are modules or libraries that do not contain a main

Description

This option affects a Code Prover analysis only.

Specify that Polyspace^® must generate a main function if it does not find one in the source files.

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 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 this option.

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

For the analogous option for model generated code, see Verify model generated code (-main-generator).

Why Use This Option

Use this option if you are verifying a module or library. A Code Prover analysis requires a main function. When verifying a module or library, your code might not have a main.

When you use this option, Code Prover generates a main function if one does not exist. If a main exists, the analysis uses the existing main.

Settings

On (default)

Polyspace generates a main function if it does not find one in the source files. The generated main:

1. Initializes variables specified by Variables to initialize (-main-generator-writes-variables).

2. Before calling other functions, calls the functions specified by Initialization functions (-functions-called-before-main).

3. In all possible orders, calls the functions specified by Functions to call (-main-generator-calls).

4. (C++ only) Calls class methods specified by Class (-class-analyzer) and Functions to call within the specified classes (-class-analyzer-calls).

If you do not specify the function and variable options above, the generated main:

• Initializes all global variables except those declared with keywords const and static.

• In all possible orders, calls all functions that are not called anywhere in the source files. Polyspace considers that global variables can be written between two consecutive function calls. Therefore, in each called function, global variables initially have the full range of values allowed by their type.

Off

Polyspace stops if a main function is not present in the source files.

Tips

• If a main function is present in your source files, the verification uses that main function, irrespective of whether you enable or disable this option.

  The option is relevant only if a main function is not present in your source files.

• If you use the option Verify whole application (default on the command line), your code must contain a main function. Otherwise you see the error:

  Error: required main procedure not found

  If your code does not contain a main function, use this option to generate a main function.

• If you specify multitasking options, the verification ignores your specifications for main generation. Instead, the verification introduces an empty main function.

  For more information on the multitasking options, see Configuring Polyspace Multitasking Analysis Manually.

Command-Line Information

Parameter: -main-generator

Default: Off

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

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