Inputs and Stubbing

Specify ranges for global variables and functions

To specify local assumptions, use the inputs and stubbing options. For instance, you can constrain ranges of some variables from external sources, or stub some imprecisely-analyzed functions for more precise analysis. The assumptions help narrow down the focus of your review to analysis results that are more meaningful. For global assumptions that apply to a certain code construct in all files and functions, use the Verification Assumptions options.

Polyspace Options

expand all

Constraint setup (-data-range-specifications)Constrain global variables, function inputs and return values of stubbed functions
Ignore default initialization of global variables (-no-def-init-glob)Consider global variables as uninitialized unless explicitly initialized in code
Functions to stub (-functions-to-stub)Specify functions to stub during analysis
Generate stubs for Embedded Coder lookup tables (-stub-embedded-coder-lookup-table-functions)Stub autogenerated functions that use lookup tables and model them more precisely
Libraries used (-library)Specify libraries that you use in your program (Since R2021a)

Polyspace Macros

unchecked_assertConstrain variable ranges for static analysis with Polyspace products

Topics