检查行为

修改运行时检查的默认行为

要修改运行时检查的默认行为，请使用检查行为选项。例如，默认情况下，溢出检查仅检测有符号整数计算中的溢出。您可以指定检查还必须检测无符号整数计算中的溢出。

Polyspace 选项

`允许左移负操作数 (-allow-negative-operand-in-shift)`	Allow left shift operations on a negative number
`有符号整数的溢出模式 (-signed-integer-overflows)`	Specify whether result of overflow is wrapped around or truncated
`无符号整数的溢出模式 (-unsigned-integer-overflows)`	Specify whether result of overflow is wrapped around or truncated

`禁用非初始化检查 (-disable-initialization-checks)`	Disable checks for non-initialized variables and pointers
`检查全局变量在热重启后是否初始化 (-check-globals-init)`	Check that global variables are assigned values in designed initialization code

`检测工作域外的堆栈指针解引用 (-detect-pointer-escape)`	Find cases where a function returns a pointer to one of its local variables
`启用跨字段的指针算术 (-allow-ptr-arith-on-struct)`	Allow arithmetic on pointer to a structure field so that it points to another field
`允许不完全或部分分配结构体 (-size-in-bytes)`	Allow a pointer with insufficient memory buffer to point to a structure
`宽松函数指针调用 (-permissive-function-pointer)`	Allow type mismatch between function pointers and the functions they point to

检测未调用的函数 (-uncalled-function-checks) Detect functions that are not called directly or indirectly from main or another entry point function

`考虑非有限浮点数 (-allow-non-finite-floats)`	Enable an analysis mode that incorporates infinities and NaNs
`无穷 (-check-infinite)`	Specify how to handle floating-point operations that result in infinity
`NaNs (-check-nan)`	Specify how to handle floating-point operations that result in NaN
`次正规数值检测模式 (-check-subnormal)`	Detect operations that result in subnormal floating-point values

`启用影响分析 (-impact-analysis)`	Check for presence or absence of impact between program elements designated as sources and sinks (自 R2023b 起)
`指定源点和汇点 (-impact-specifications)`	Specify XML file that identifies program elements as sources and sinks for impact analysis (自 R2023b 起)
`仅显示影响分析结果 (-impact-analysis-only)`	Skip regular Code Prover checks for run-time errors and perform impact analysis only (自 R2023b 起)

计算堆栈使用量 (-stack-usage) 计算并显示堆栈使用量的估计值 (自 R2022a 起)

指定 Polyspace 分析选项
在 Polyspace^® 用户界面、其他 IDE 或脚本中指定 Polyspace 分析选项。
Modify or Disable Code Prover Run-Time Checks

Disable a subset of run-time checks in Code Prover.
- Modify Code Prover Run-Time Checks Through Code Behavior Specifications
Detect Overflows in Buffer Size Computation
Detect overflows earlier during buffer size computation instead of later during buffer usage.

Prove Absence of Impact Between Objects in C/C++ Program
Set up impact analysis in Polyspace Code Prover™, define sources and sinks.
Source and Sink Specifications for Impact Analysis in Polyspace Code Prover
Look up XML syntax for designating variables and function arguments as sources and sinks.
Event and Memory Zone Specifications for Impact Analysis in Polyspace Code Prover
Look up XML syntax for specifying events and memory zones associated with impact sinks.