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