随着互联网的迅速发展,信息化已经覆盖了生活的方方面面,但也随之带来了很多问题,例如黑客攻击造成的信息泄露和经济损失等,因此可信软件的研发已成为当务之急。静态分析是发现软件源代码缺陷和提高软件源代码质量的有效方式。然而,静态分析由于不实际运行代码,无法收集足够的数据流信息,故其分析结果存在精确性偏低的情况。符号执行技术通过模拟程序的执行能够收集足够的数据流信息,从而增加数据流分析的精确性,弥补静态分析工具的缺陷。为了提高静态分析结果的精确性,本文设计并实现了一个源代码缺陷检测工具ABAZER-SE,它基于GCC抽象语法树,组合采用符号执行与静态分析技术以检测源代码中的缺陷。本文主要的研究内容和工作成果如下:(1)研究了 GCC抽象语法树编码类型、静态分析方法及符号执行技术工作原理,深入分析了基于缺陷模式静态分析技术的特点,提出了利用符号执行技术提高静态分析检测结果精确性的方案。(2)本文设计了用于符号执行的路径探索算法、语句分析算法以及关键数据结构。设计了特定的链表结构用于处理不确定数组下标和不确定指向的指针,使分析结果更加精确。(3)为了实现不同语句类型的语义模拟,本文构建了包含栈、堆和静态存储区域的内存模型,可以在构建的内存模型中进行数据流信息的提取和存储。实现了 Z3约束求解器的路径约束条件的形式转换,可以方便地对路径条件进行约束求解。(4)本文使用ABAZER-SE对Juliet测试集、Toyota ITC静态分析基准、Coreutils 软件进行 了测试,并与 ABAZER、Cppcheck、KLEE进行了对比分析,实验结果表明它能够有效地检测源代码中的缺陷。