Provide Context for C++ Code Verification

This example shows how to provide context to your C++ code verification. If you use default options and do not provide a main function, Polyspace^® Code Prover™ checks your code for robustness against all verification conditions. For instance, the software:

Considers that global variables and inputs of uncalled functions and methods are full range.
Generates a main that calls uncalled functions in arbitrary order.

In addition, if you do not define a function but declare and call it in your code, Polyspace stubs the function. For a detailed list of assumptions, see Code Prover Analysis Assumptions.

You can use analysis options on the Configuration pane to change the default behavior and provide more context about your code. Performing contextual verification can result in more proven code and therefore fewer orange checks.

Control Variable Range

Use the following options. In the user interface of the Polyspace desktop products, the options appear under the Code Prover Verification node.

Option	Purpose
`Variables to initialize (-main-generator-writes-variables)`	Specify the global variables that Polyspace must consider as initialized despite no explicit initialization in the code.
`Constraint setup (-data-range-specifications)`	Specify range for global variables.

Control Function Call Sequence

Use the following options to call class methods. In the user interface of the Polyspace desktop products, the options appear under the Code Prover Verification node.

Option	Purpose
`Class (-class-analyzer)`	Specify classes whose methods the generated `main` must call.
`Functions to call within the specified classes (-class-analyzer-calls)`	Specify methods that the generated `main` must call.
`Analyze class contents only (-class-only)`	Specify that the generated `main` must call class methods only.
`Skip member initialization check (-no-constructors-init-check)`	Specify that the generated `main` must not check whether each class constructor initializes all class members.

Use the following options to call functions that are not class methods. In the user interface of the Polyspace desktop products, the options appear under the Code Prover Verification node.

Option	Purpose
`Initialization functions (-functions-called-before-main)`	Specify the functions that the generated `main` must call first.
`Functions to call (-main-generator-calls)`	Specify the functions that the generated `main` must call later.

Documentation