验证假设
配置关于源代码的软件假设
要指定有关特定代码构造的全局假设,请使用验证假设选项。例如,指定所有外部指针均可能为 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 起) |
主题
- 指定 Polyspace 分析选项
在 Polyspace® 用户界面、其他 IDE 或脚本中指定 Polyspace 分析选项。