Provide Context for C Code Verification

This example shows how to provide context for 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 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. 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.

Control Stubbing Behavior

Use the following options. In the user interface of the Polyspace desktop products, the options appear under the Inputs & Stubbing node.

Option	Purpose
`Functions to stub (-functions-to-stub)`	Specify the functions that Polyspace must stub.