配置运行时检查

修改 Polyspace^® 运行时检查的行为

配置 Polyspace 分析您的代码并检查运行时错误的方式：

Polyspace 选项

`允许左移负操作数 (-allow-negative-operand-in-shift)`	允许对负数执行左移位运算
`有符号整数的溢出模式 (-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
`-show-similar-overflows`	以绕回模式显示所有溢出

`检测工作域外的栈指针解引用 (-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) 检测未直接或间接被 main 或另一个入口函数调用的函数

`考虑非有限浮点数 (-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

-code-behavior-specifications Associate behaviors with code elements such as functions

-check-parameter-of-stubbed-functions Enable checking pointer parameters of stubbed functions

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.