3.1.3　路径约束提取

路径约束在CTS中定义成如下的表达式(在本书中,路径约束和表达式表示的意义相同)形式:

从表达式的定义可以看出,表达式能处理加减乘除四则运算,并能处理乘方运算,除此之外的其他算术运算都被认为是复杂算术表达式,如a%b,因为在表达式的产生式定义中没有出现%(取模)运算。目前区间运算无法求出复杂表达式的值,而是为复杂表达式生成一个新的符号,并给新生成的符号分配一个更大的区间。在分支限界中,为了处理这类复杂表达式,专门开发了一个反函数库,对于出现的类似复杂运算可以分别处理。

由于区间运算的过程不需要提取表达式,因此没有提供获取表达式的接口。为了提取表达式,必须在区间运算之前把所有的表达式暂存起来。基于此思想,修改了区间运算部分的代码,在表达式进行区间运算之前,将表达式存储在控制流图节点中。由于路径是由控制流图节点组成的,因此提取含有表达式的控制流图节点就相当于提取了表达式。下面是从中提取含有表达式的控制流图节点的算法。该算法的流程如图3-3所示,算法描述如下。

①在算法开始执行前定义一个线性链表explist存储含有表达式的控制流图节点。(https://www.daowen.com)

②若路径p中还有控制流图节点未被访问,则依次取路径p中的一个控制流图节点node,转去执行③;否则,返回explist,算法结束。

③若node中含有表达式,则将该node存储到explist中,转去执行②;若node中不含表达式,则转去执行②。

图3-3　表达式提取算法流程图