基于抽象解释的单变量值范围分析

摘要

cqvip:针对传统基于抽象解释的变量值范围分析方法存在覆盖代码程度不高的问题,提出了一种新的描述单变量值区间方法。该方法采用找到数值型子程序的矛盾结点,全面考虑了不同的选择结构和循环结构的嵌套,并考虑了分析精度与效率的问题。以抽象解释理论作为分析框架,研究程序中各个变量的上下文状态,达到验证程序变量是否满足规范的目的。利用公开已有的变量值范围数据对变量值范围分析方法进行的验证表明,与现有的值范围分析方法相比,该方法由于更全面地考虑了不同的嵌套结构,因此取得了更好的结果。