C程序精确形状分析中的规范语言设计

摘要：

在一个C程序静态分析工具的实现中,设计了一种描述函数行为的规范语言,包括描述程序状态的基本断言,描述内存的谓词以及描述链表、二叉树等递归数据结构的形状谓词.该工具基于编译框架LLVM和符号执行工具KLEE,以函数为单位分析并构造函数行为规范,该过程中需要使用断言描述程序状态并按需抽象成形状谓词表示的形式.为此本文设计并实现了一系列的断言规范化和抽象化规则.通过使用描述内存的谓词以及形状谓词,该分析工具可以检测内存泄露、多次释放等内存安全问题以及进行形状分析.

关键词：符号执行、规范语言、形状分析、规范化、抽象化

所属期刊栏目：37

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金面上项目61170018

在线出版日期：2016-10-25（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：653-658