Verification Assumptions

Configure software assumptions about source code

To specify global assumptions about a specific code construct, use the verification assumption options. For instance, specify that all external pointers can possibly be NULL or the volatile qualifier on all structure fields must be considered. For local assumptions that apply to specific variables, functions or files, use the Inputs & Stubbing options.

For a more complete list of assumptions, see Code Prover Analysis Assumptions.

Polyspace Options

`Float rounding mode (-float-rounding-mode)`	Specify rounding modes to consider when determining the results of floating point arithmetic
`Consider environment pointers as unsafe (-stubbed-pointers-are-unsafe)`	Specify that environment pointers can be unsafe to dereference unless constrained otherwise
`Consider volatile qualifier on fields (-consider-volatile-qualifier-on-fields)`	Assume that `volatile` qualified structure fields can have all possible values at any point in code
`Ignore assembly code (-ignore-assembly-code)`	Specify that assembly instructions in C/C++ code cannot modify C/C++ variables (Since R2023a)

Topics

Specify Polyspace Analysis Options
Specify Polyspace^® analysis options in Polyspace user interface, other IDE-s or scripts.