输入和插桩

指定全局变量和函数的范围

要指定局部假设，请使用输入和插桩选项。例如，您可以对外部来源中某些变量的范围设定约束，或者对某些分析不精确的函数插桩以实现更精确的分析。这些假设有助于您将审查重点的范围缩小到更有意义的分析结果。对于适用于所有文件和函数中的特定代码构造的全局假设，请使用验证假设选项。

Polyspace 选项

`约束设置 (-data-range-specifications)`	对插桩函数的全局变量、函数输入和返回值进行约束
`忽略全局变量的默认初始化 (-no-def-init-glob)`	Consider global variables as uninitialized unless explicitly initialized in code

`要插桩的函数 (-functions-to-stub)`	Specify functions to stub during analysis
`为 Embedded Coder 查找表生成桩件 (-stub-embedded-coder-lookup-table-functions)`	Stub autogenerated functions that use lookup tables and model them more precisely
`使用的库 (-library)`	Specify libraries that you use in your program (自 R2021a 起)

unchecked_assert Constrain variable ranges for static analysis with Polyspace products

指定 Polyspace 分析选项
在 Polyspace^® 用户界面、其他 IDE 或脚本中指定 Polyspace 分析选项。
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.
- XML File Format for Polyspace Analysis Constraints
Test Functions and Constrain Polyspace Code Prover Analysis for Ranges of Inputs and Outputs (Polyspace Test)
Test functions over one or more ranges of input and verify if the output is within a valid range using range specification macros. Run static analysis on the function and associated tests using the specified ranges as external constraint.
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().