Inputs and Stubbing
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
Polyspace Macros
unchecked_assert | Constrain variable ranges for static analysis with Polyspace products |
Topics
- Specify Polyspace Analysis Options
Specify Polyspace® analysis options in Polyspace user interface, other IDE-s or scripts.
- Specify External Constraints for Polyspace Analysis
Constrain variable ranges and pointer specifications for more precise analysis.
- External Constraints for Polyspace Analysis
Look up constraints that you can apply on global variables, function inputs and stubbed functions.
- Provide Context for C Code Verification
Learn what external context you can provide to narrow down the default verification assumptions.
- Provide Context for C++ Code Verification
Learn what external context you can provide to narrow down the default verification assumptions.
- Constrain Variable Ranges for Polyspace Analysis Using Manual Stubs and Manual main() Function
Improve precision of Polyspace Code Prover™ analysis using your own stubs and
main()
.