Initialization functions (-functions-called-before-main)

Specify functions that you want the generated main to call ahead of other functions

Description

This option affects a Code Prover analysis only.

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

Specify functions that you want the generated main to call ahead of other functions.

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 enter values 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 enter values for this option. See Dependencies for other options you must enable first.

  • Command line and options file: Use the option -functions-called-before-main. 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.

Use this option along with the option Functions to call (-main-generator-calls) to specify which functions the generated main must call. Unless a function is called directly or indirectly from main, the software does not analyze the function.

Settings

No Default

Enter function names or choose from a list.

  • Click to add a field and enter the function name.

  • Click to list functions in your code. Choose functions from the list.

If the function or method is not overloaded, specify the function name. Otherwise, specify the function prototype with arguments. For instance, in the following code, you must specify the prototypes func(int) and func(double).

int func(int x) { 
 return(x * 2);
}
double func(double x) { 
 return(x * 2);
}
For C++, if the function is:

  • A class method: The generated main calls the class constructor before calling this function.

  • Not a class method: The generated main calls this function before calling class methods.

If you use the scope resolution operator to specify the function from a particular namespace, enter the fully qualified name, for instance, myClass::init(int). If the function does not have a parameter, use an empty parenthesis, for instance, myClass::init().

Dependencies

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

The option is ignored if your code contains a main function.

Tips

Although these functions are called ahead of other functions, they can be called in arbitrary order. If you want to call your initialization functions in a specific order, manually write a main function to call them.

Command-Line Information

Parameter: -functions-called-before-main
Value: function1[,function2[,...]]
No Default
Example 1 (Code Prover): polyspace-code-prover -sources file_name -main-generator -functions-called-before-main myfunc
Example 2 (Code Prover): polyspace-code-prover -sources file_name -main-generator -functions-called-before-main myClass::init(int)
Example 1 (Code Prover Server): polyspace-code-prover-server -sources file_name -main-generator -functions-called-before-main myfunc
Example 2 (Code Prover Server): polyspace-code-prover-server -sources file_name -main-generator -functions-called-before-main myClass::init(int)

See Also

| | | |

Topics