配置分析精度

配置 Code Prover 假设和验证精度

使用精度选项配置验证精度。更高精度的验证会产生更少的橙色检查，但需要更多计算资源。您可以配置：

  • 全局精度 - 指定影响引擎级别精度的选项。这些精度选项可能影响任何 Polyspace® Code Prover™ 分析。

  • 文件和函数 - 这些选项指定 Code Prover 分析函数和源文件的方式。

  • 数组和指针 - 这些选项指定对数组和指针进行建模和分析的方式。

  • 汇编代码 - 这些选项指定处理汇编函数的方式。

Polyspace 选项

全部展开

精度等级 (-O0 | -O1 | -O2 | -O3)指定用于验证的精度等级
验证等级 (-to)Specify number of times the verification process runs on your code
验证时限 (-timeout)指定分析的时间限制
敏感度上下文 (-context-sensitivity)Store call context information to identify function call that caused errors
提高过程间分析的精度 (-path-sensitivity-delta)Avoid certain verification approximations for code with fewer lines
特定精度 (-modules-precision)指定要以比其余验证更高的精度进行验证的源文件
-consider-external-array-access-unsafe删除未指定大小的外部数组可以按任何索引安全访问的默认假设
-improve-pointer-analysis-precisionEnable more precise pointer analysis mode in Code Prover (自 R2022a 起)
-no-assumption-on-absolute-addressesRemove assumption that absolute address usage is valid
将环境指针视为不安全 (-stubbed-pointers-are-unsafe)Specify that environment pointers can be unsafe to dereference unless constrained otherwise
-consider-external-array-access-unsafe删除未指定大小的外部数组可以按任何索引安全访问的默认假设
-improve-pointer-analysis-precisionEnable more precise pointer analysis mode in Code Prover (自 R2022a 起)
-asm-begin -asm-end将编译器特定的 asm 函数排除在分析之外
忽略汇编代码 (-ignore-assembly-code)Specify that assembly instructions in C/C++ code cannot modify C/C++ variables (自 R2023a 起)
忽略汇编代码 (-ignore-assembly-code)Specify that assembly instructions in C/C++ code cannot modify C/C++ variables (自 R2023a 起)
-code-behavior-specificationsAssociate behaviors with code elements such as functions
浮点数舍入模式 (-float-rounding-mode)Specify rounding modes to consider when determining the results of floating point arithmetic
考虑字段的 volatile 限定符 (-consider-volatile-qualifier-on-fields)Assume that volatile qualified structure fields can have all possible values at any point in code

主题

相关信息