本页翻译不是最新的。点击此处可查看最新英文版本。

约束设置 (-data-range-specifications)

对插桩函数的全局变量、函数输入和返回值进行约束

全页展开

描述

使用约束设定模板文件为插桩函数的全局变量、函数输入和返回值设定约束（也称为数据范围设定 (DRS)）。该模板文件是一个 XML 文件，您可以在 Polyspace® 用户界面中生成该文件。

设置选项

用户界面（仅限桌面端产品）：在您的工程配置中，此选项位于输入和插桩节点上。

用户界面（仅限 Polyspace 平台、桌面端产品）：在您的工程配置中，此选项位于输入和插桩节点的静态分析选项卡上。

命令行和选项文件：请使用 -data-range-specifications 选项。请参阅命令行信息。

为何使用此选项

代码中某些对象的值只有在运行时才会确定（例如用户输入或传感器值），使用此选项可对这类对象进行约束。使用正确约束的对象可以减少 Polyspace 结果中的误报或橙色检查项。

Polyspace 会根据您的源代码对变量范围和允许的指针缓冲区大小等项做出假设。有时，这些假设比您预期的更宽泛，原因如下：

  • 您没有提供完整的代码。例如，您没有提供某些函数定义。

  • 变量的某些信息只有在运行时才能获知。例如，代码中的某些变量需要在运行时从用户那里获取值。

例如，表示真实世界速度的 int 变量的值不能小于零或大于光速。Polyspace 可能会假设该变量的范围为 [-2^32... 2^32-1]。这些宽泛的假设可能会导致以下结果：

  • Code Prover 考虑的执行路径可能会比运行时实际出现的更多。如果沿其中一条执行路径的运算失败，则 Polyspace 会将该运算标记为橙色检查项。如果该执行路径在运行时并未出现，该橙色检查项将显示为误报。

  • Bug Finder 可能会生成误报。

要减少这类误报的数量，请为插桩函数的全局变量、函数输入和返回值设定适用的约束。

在设定约束后，将它们保存为 XML 文件，以便用于后续分析。如果您的源代码发生更改，请更新先前的约束。不需要创建新的约束模板。

设置

无默认值

输入模板文件的完整路径。或者，点击 以打开约束设定向导。使用此向导可以生成模板文件或导航到现有的模板文件。

有关详细信息，请参阅Specify External Constraints for Polyspace Analysis。

命令行信息

参数：-data-range-specifications
值：file
无默认值
示例 (Bug Finder)：polyspace-bug-finder -sources file_name -data-range-specifications "C:\DRS\range.xml"
示例 (Code Prover)：polyspace-code-prover -sources file_name -data-range-specifications "C:\DRS\range.xml"
示例 (Bug Finder Server)：polyspace-bug-finder-server -sources file_name -data-range-specifications "C:\DRS\range.xml"
示例 (Code Prover Server)：polyspace-code-prover-server -sources file_name -data-range-specifications "C:\DRS\range.xml"

您可以指定约束文件的绝对路径，也可以指定一个相对路径（相对于您要从中运行 polyspace-bug-finder 或 polyspace-code-prover 命令的位置）。

示例

全部展开

在以下代码中，tmp 的定义中的乘法运算具有橙色的溢出检查。之所以会出现此检查，是因为 Polyspace 假设 getSpeed() 函数的返回值范围为 -2^32... 2^32-1。

//file1.c
extern int getSpeed(); //Returns the reading of speedometer
int main(){
	//...
	int tmp = 2* getSpeed();
	//...
	return 0;
}

要解决此橙色检查项问题，请将 getSpeed() 的返回值的范围约束为 [0..30000000]。创建包含以下内容的 XML 文件 drs.xml：

<?xml version="1.0" encoding="UTF-8"?>
<!--EDRS Version 2.0-->
<global>
	<file name="C:\\Users\\example.c">
		<function name="getSpeed"
				  line="1"
				  attributes="extern"
				  main_generator_called="disabled"
				  comment="">
			<scalar name="return"
					line="1"
					base_type="int32"
					complete_type="int32"
					init_mode="PERMANENT"
					init_modes_allowed="4"
					init_range="0  30000000"
					global_assert="unsupported"
					assert_range="unsupported"
					comment=""/>
		</function>
	</file>
</global>

在指定数据范围后，再次运行验证。请使用以下命令：

polyspace-code-prover file1.c -data-range-specifications drs.xml -lang c
此橙色检查项已被绿色检查项所替换。
extern int getSpeed(); //Returns the reading of speedometer
int main(){
	//...
	int tmp = 2* getSpeed();
	//...
	return 0;
}

另请参阅

|

主题