Main Content

Verify initialization section of code only (-init-only-mode)

Check initialization code alone for run-time errors and other issues

Since R2020a

Description

This option affects a Code Prover analysis only.

Specify that Polyspace® must check only the section of code marked as initialization code for run-time errors and other issues.

The initialization code depends on the source code you verify:

  • When verifying whole application — The initialization code starts from the beginning of the main() function and continues up to this #pragma directive:

    #pragma polyspace_end_of_init
    You cannot specify this #pragma more than once. Since compilers ignore unrecognized pragmas, the presence of this pragma does not affect program execution.

  • When verifying modules or libraries — The initialization code is the sequence of functions called before the generated main. Specify these function by using the option Initialization functions (-functions-called-before-main). Polyspace assumes that the initialization functions are called in the same sequence in which they are specified.

Set Option

User interface (desktop products only): In your project configuration, the option is on the Code Prover Verification node.

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 -init-only-mode. See Command-Line Information.

Why Use This Option

Often, issues in the initialization code can invalidate the analysis of the remaining code. You can use this option to check the initialization code alone and fix the issues, and then disable this option to verify the remaining program.

Consider these examples:

  • Verifying whole application — This example code contains a main() function and is considered a complete application. The end of initialization code is indicated by the pragma directive polyspace_end_of_init. 

    #include <limits.h>

int aVar;
const int aConst = INT_MAX;
int anotherVar;

int main() {
      aVar = aConst + 1;
#pragma polyspace_end_of_init
      anotherVar = aVar - 1;
      return 0;
}
    The overflow in the line aVar = aConst+1 must be fixed first before the value of aVar is used in subsequent code.

  • Verifying modules or libraries — This example code does not contain a main() function and is considered a module or a library. The initialization code and their sequence is specified by the option Initialization functions (-functions-called-before-main).

    #include <limits.h>

int aVar;
const int aConst = INT_MAX;
int anotherVar;

void initialize() {
	aVar = aConst + 1;
}

int foo() {
	anotherVar = aVar - 1;
	return 0;
}
    The overflow in the line aVar = aConst+1 must be fixed first before the value of aVar is used in subsequent code. For this example, use this command:
    polyspace-code-prover -sources src.c -init-only-mode -main-generator -functions-called-before-main initialize

Settings

On

Polyspace checks the code from the beginning of main and continues up to the pragma polyspace_end_of_init.

Off (default)

Polyspace checks the complete application beginning from the main function.

Dependencies

Tips

  • Use this option along with the option Check that global variables are initialized after warm reboot (-check-globals-init) to thoroughly check the initialization code before checking the remaining program. If you use both options, the verification checks for the following:

    • Definite or possible run-time errors in the initialization code.

    • Whether all non-const global variables are initialized along all execution paths through the initialization code.

  • Multitasking options are disabled if you check initialization code only because the initialization of global variables is expected to happen before the tasks (threads) begin. As a result, task bodies are not verified.

    See also Multitasking.

  • If you check initialization code only, the analysis truncates execution paths containing the pragma at the location of the pragma but continues to check other execution paths.

    For instance, in this example, the pragma appears in an if block. A red non-initialized variable check appears on the line int a = var because the path containing the initialization stops at the location of the pragma. On the only other remaining path that bypasses the if block, the variable var is not initialized.

    int var;

int func();

int main() {
    int err = func();
    if(err) {
        var = 0;
 #pragma polyspace_end_of_init
    }
    int a = var;   
    return 0;
}
    To avoid these situations, place the pragma outside a block. For more suggestions for the placement of the directive, see Check that global variables are initialized after warm reboot (-check-globals-init).

  • To determine the initialization of a structure, a regular Code Prover analysis only considers fields that are used.

    If you check initialization code only using this option, the analysis covers only a portion of the code and cannot determine if a variable is used beyond this portion. Therefore, the checks for initialization consider all structure fields, whether used or not.

Command-Line Information

Parameter: -init-only-mode
Default: Off
Example (Code Prover): polyspace-code-prover -sources file_name -init-only-mode
Example (Code Prover Server): polyspace-code-prover-server -sources file_name -init-only-mode

Version History

Introduced in R2020a

expand all

See Also

| | |

Topics