基于CEGAR的C程序空指针解引用检测

摘要

随着计算机硬件技术的发展，计算机软件系统的复杂性越来越高，所涉及的代码量越来越大，同时程序中的错误和问题隐患也越来越多。因此，如何提高软件系统的可靠性和安全性已成为计算机软件领域的一个紧迫需求。
　　软件模型检测技术是提高程序可靠性和安全性的重要途径。该技术可以自动化地验证程序是否可以满足一些关键性质。C语言是目前软件领域最为广泛使用的编程语言之一。它的语法规范比较灵活，尤其是对指针的使用，稍微不注意，就会导致程序崩溃。在C程序中，对指针的不正确使用，会带来如内存泄露，指针未初始化、多次释放，以及空指针解引用等问题。本文研究基于CEGAR技术的C程序空指针解引用的检测算法。首先，实现了基于CEGAR的C程序PPTL模型检测算法。在此基础上，通过PPTL公式来描述空指针解引用的特征，进一步检测C程序中是否存在空指针解引用的问题。为了提高验证的自动化水平，本文通过对C源代码进行扫描，对所涉及到的指针自动产生待验证的PPTL性质，避免了手动在C程序中加入断言所带来的麻烦。在以上方法的基础上，实现了基于CEGAR的C程序PPTL模型检测检测工具：PPTLChecker。该工具可以支持PPTL公式描述的程序性质的验证，实现了对程序中空指针解引用问题的自动化检测功能。实验结果表明，PPTLChecker在C程序空指针解引用检测中有着实际的应用价值。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 绪论

1.1研究的背景和意义

1.2模型检测技术的发展与现状

1.3研究内容和目标

1.4论文结构

第二章 相关技术与工具

2.1模型检测

2.2模型检测算法

2.3相关技术与工具

2.4本章小结

第三章 基于CEGAR的C程序PPTL模型检测

3.1命题与性质的生成

3.2命题的转换

3.3性质的转换

3.4 ARG的生成过程

3.5后继状态求解

3.6查找反例路径和细化

3.7本章小结

第四章 空指针解引用检测

4.1指针变量的提取

4.2计算ARGState的命题

4.3优化操作

4.4本章小结

第五章 实验结果分析

5.1算法的实现效果

5.2可视化工具

5.3实例演示

5.4本章小结

第六章 总结和展望

参考文献

致谢

作者简介