一种基于变量可达向量的链表抽象方法

提出了一种链表抽象表示方法.该方法隐式存储链表结点之间的边信息,并采用了一种紧致的链表状态表示,存储开销较低,且维护了链表长度信息,精确度较高.具体而言,根据变量对链表结点的可达性质定义了变量可达向量,采用带计数的变量可达向量集描述链表的形态及数量性质,并定义了基本链表操作的抽象语义.通过简单扩展,该方法可以建模包括环形链表在内的所有单向链表.最后,为了验证该链表抽象方法的正确性,在符号执行框架中进行实验,并对常见链表操作程序的运行时错误、长度相关性质等关键性质进行了分析与验证.