验证假设

配置关于源代码的软件假设

要指定有关特定代码构造的全局假设，请使用验证假设选项。例如，指定所有外部指针均可能为 NULL 或者必须考虑所有结构体字段上的 volatile 限定符。对于适用于特定变量、函数或文件的局部假设，请使用输入和插桩选项。

有关更完整的假设列表，请参阅 Code Prover 分析假设。

Polyspace 选项

`浮点数舍入模式 (-float-rounding-mode)`	Specify rounding modes to consider when determining the results of floating point arithmetic
`将环境指针视为不安全 (-stubbed-pointers-are-unsafe)`	Specify that environment pointers can be unsafe to dereference unless constrained otherwise
`考虑字段中的 volatile 限定符 (-consider-volatile-qualifier-on-fields)`	Assume that `volatile` qualified structure fields can have all possible values at any point in code
`忽略汇编代码 (-ignore-assembly-code)`	Specify that assembly instructions in C/C++ code cannot modify C/C++ variables (自 R2023a 起)