为 Polyspace 分析的全局变量范围设定约束
您可以对 C/C++ 代码中全局变量的范围施加外部约束（也称为数据范围规范 (DRS)），并通过 Polyspace® Code Prover™ 检查对变量的写入操作是否违反了约束。有关常规工作流，请参阅Specify External Constraints for Polyspace Analysis。
用户界面（仅限桌面端产品）
要为全局变量范围设定约束并检查违反该约束的情形，请执行以下操作：
在您的工程配置中，选择输入和插桩。点击约束设置字段旁边的
按钮。在“约束设定”窗口中，点击
。在全局变量节点下，您会看到全局变量的列表。
针对您要设定约束的全局变量，请执行以下操作：
从全局断言列的下拉列表中，选择是。
在全局断言范围列中，以
min..maxmin是全局变量的最小值，max是全局变量的最大值。
要保存您的设定，请点击
按钮。在保存约束文件窗口中，将您输入的内容保存为
xml文件。运行验证并打开结果。
对于针对全局变量的每个写入操作，您会看到一个显示为绿色、橙色或红色的正确性判定条件检查。如果此检查为：
绿色，则说明变量在您设定的范围内。
橙色，则说明变量可能在您设定的范围外。
红色，则说明变量在您设定的范围外。
当有两个或更多任务向同一全局变量执行写入时，即使只有一个写入操作会使该变量超出全局断言范围，正确性判定条件检查也会在对该变量的所有写入操作中显示为橙色。
命令行
将约束设置 (-data-range-specifications) 选项与设定约束的 XML 文件一起使用。
例如，对于通过 Polyspace Code Prover Server™ 进行的分析，请按如下所示指定该选项：
polyspace-code-prover-server -sources filename -data-range-specifications "C:\Polyspace\drs_project1.xml"
按照Specify External Constraints for Polyspace Analysis中所述创建一个空白的约束 XML 模板。在 XML 文件中，找到全局变量并为它们设定约束。全局变量的 XML 标记直接显示在 file 标记内，没有外围的 function 标记。例如，在以下约束 XML 文件中，PowerLevel 和 SHR 是全局变量：
<file name="\\\\home\\johndoe\\Documents\\Polyspace_Workspace\\Examples\\Code_Prover_Example\\sources\\tasks1.c">
<scalar name="PowerLevel" line="26" ... global_assert="YES" assert_range="0..10" />
<scalar name="SHR" line="30" ... global_assert="NO" assert_range="" />
<function name="Tserver" line="73" .../>
<function name="initregulate" line="47" .../>
<function name="orderregulate" line="35" ...>
<scalar name="return" ... global_assert="unsupported" assert_range="unsupported" />
</function>
<function name="proc1" line="101" .../>
</file>要为某个全局变量设定约束并在 Code Prover 分析期间检查是否违反了该约束，请执行以下操作：
将该变量的
scalar标记的global_assert属性设置为YES。将
assert_range属性设置为min..max0..10。
在前面的示例中，就是用这种方式为变量 PowerLevel 设定约束的。
另请参阅
Polyspace 分析选项
Polyspace 结果
正确性判定条件(Polyspace Code Prover)
