主要内容

验证假设

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

要指定有关特定代码构造的全局假设,请使用验证假设选项。例如,指定所有外部指针均可能为 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 起)

主题