主要内容

特定精度 (-modules-precision)

指定要以比其余验证更高的精度进行验证的源文件

描述

此选项仅影响 Code Prover 分析。

指定要以高于整体验证的精度级别进行验证的源文件。

设置选项

使用以下方法之一设置选项:

  • Polyspace 平台用户界面(仅限桌面端产品):在您的工程配置中,在静态分析选项卡上选择运行时错误 > 精度节点,然后为此选项输入值。有关您必须先启用的其他选项,请参阅依赖关系

  • 命令行和选项文件:请使用 -modules-precision 选项。请参阅命令行信息

为何使用此选项

如果特定文件因验证不精确导致该文件和其他位置出现大量橙色检查,您可以提高该文件的精度。

请注意,提高精度会同时增加验证时间。

设置

默认值:所有文件使用您通过精度 > 精度等级指定的精度进行验证。

点击 ,输入不含扩展名 .c 的文件名及对应的精度等级。

依赖关系

仅在您将源代码语言 (-lang) 设置为 CC-CPP 时,此选项才可用。

命令行信息

参数:-modules-precision
值:file:O0 | file:O1 | file:O2 | file:O3
示例 (Code Prover):polyspace-code-prover -sources file_name -O1 -modules-precision My_File:O2
示例 (Code Prover Server):polyspace-code-prover-server -sources file_name -O1 -modules-precision My_File:O2