5.3.5　实例分析

本节以文献[24]中的程序isEasyChair()为例,介绍利用本章提出的技术生成字符串测试用例的过程。为了便于理解,示例程序中的字符串函数被重命名为C语言库函数中的名称,所选择的程序路径如图5-15所示,包含和字符串相关的操作。

图5-15　示例程序中的字符串操作

首先将路径约束按照约束提取规则,以L Atom的公式的形式提取,并且分为下标约束和数组约束两部分。提取结果如表5-7所示。

对表5-7中的约束,首先为下标变量生成具体值,假设得到了一个解:{i 1:18,i 2:8,i 3:5,i 4:6,s 1:20,s 2:10,s 3:10,N :2},满足下标部分的约束。对N 赋值为2之后,应用N-Propagation规则消去约束中的N,通过引入两个下标变量n 1和n 2,将包含s 2[N]和s 3[N]的公式更新为一组包含s 2[n 1]、s 2[n 2]、s 3[n 1]和s 3[n 2]的公式。(https://www.daowen.com)

然后,根据边界变量i 3的赋值5以及i-Propagation规则,确定字符串s 2中子串“Easy”的位置。根据边界变量i 4的赋值6和i-Propagation规则,生成约束表达式为s 2[6]=&,与语句4的数组约束存在冲突,因此需要回溯到上一个状态,并且将导致矛盾的约束i 4≠6加入下标约束C p中。

当下标约束中不包含未取值的下标变量时,路径约束中仅包含关于数组的无量词的一阶表达式,接下来使用能够求解数组约束的求解器得到最后的测试用例。

表5-7　以L Atom中的公式表示的路径约束