基于区域内存模型的C程序静态分析

• 作者: 宫云战 董玉坤 邢颖 金大海
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 可寻址表达式 内存模型 静态分析 符号化函数摘要 缺陷检测
• 年，卷（期）: 2014,（2）
• 所属期刊栏目: 嵌入式系统软件设计方法与技术专刊
• 页码范围: 357-372
• 页数: 16页
• 分类号: TP311
• 字数: 13975字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.004532

摘要

为了提高程序的静态分析精度,提出了一种应用基于区域的符号化三值逻辑(region-based symbolic threevalued logic,简称RSTVL)的静态分析方法.RSTVL能够描述C程序运行时内存中数据结构的形态信息与变量的存储状态,以及可寻址表达式间的各种关系,包括指向关系、层次关系与取值逻辑关系.为了提高静态分析的精度,提出了一种基于RSTVL的流敏感、域敏感的过程内分析与基于符号化函数摘要的上下文敏感的过程间分析,能够精确地分析出每个程序点上的形态信息、数据流信息与指针指向关系.实验结果表明,相对于基于符号化三值逻辑的方法,该分析方法在保证一定分析效率的前提下,能够实现较高准确度的分析.