C程序精确形状分析中的规范语言设计
| 摘要 | 第1-6页 |
| Abstract | 第6-8页 |
| 目录 | 第8-11页 |
| 第1章 绪论 | 第11-19页 |
| ·研究背景 | 第11-16页 |
| ·C程序的安全性 | 第12-13页 |
| ·程序静态分析 | 第13-15页 |
| ·规范语言 | 第15-16页 |
| ·本文概述 | 第16-19页 |
| ·研究工作 | 第16页 |
| ·主要贡献 | 第16-17页 |
| ·章节安排 | 第17-19页 |
| 第2章 SHAPECHECKER简介 | 第19-27页 |
| ·ShapeChecker总体框架 | 第19-21页 |
| ·编译框架LLVM | 第21-24页 |
| ·LLVM总体结构 | 第21-22页 |
| ·LIVM IR简介 | 第22-24页 |
| ·符号执行 | 第24-26页 |
| ·符号执行算法 | 第25页 |
| ·符号执行面临的问题 | 第25-26页 |
| ·本章小结 | 第26-27页 |
| 第3章 规范语言的设计 | 第27-41页 |
| ·ACSL简介 | 第27-28页 |
| ·IRSL规范语言 | 第28-34页 |
| ·断言语言 | 第29-30页 |
| ·形状谓词 | 第30-32页 |
| ·函数规范 | 第32-34页 |
| ·函数行为规范的构建 | 第34-37页 |
| ·程序状态 | 第34-36页 |
| ·行为规范的构建过程 | 第36-37页 |
| ·支持的C标准库函数 | 第37-40页 |
| ·malloc()函数行为规范 | 第37-38页 |
| ·free()函数行为规范 | 第38页 |
| ·strcat()函数行为规范 | 第38-40页 |
| ·本章小结 | 第40-41页 |
| 第4章 规范化和抽象化 | 第41-53页 |
| ·规范化 | 第41-42页 |
| ·抽象化 | 第42-50页 |
| ·单链表表段的抽象规则 | 第42-44页 |
| ·双链表表段的抽象规则 | 第44-48页 |
| ·二叉树的抽象规则 | 第48-50页 |
| ·数组谓词的抽象 | 第50页 |
| ·本章小结 | 第50-53页 |
| 第5章 实例分析 | 第53-65页 |
| ·一维数组程序示例 | 第53-56页 |
| ·函数行为规范 | 第53-55页 |
| ·抽象化和规范化操作 | 第55-56页 |
| ·单链表的程序示例 | 第56-59页 |
| ·函数行为规范 | 第56-57页 |
| ·抽象化操作 | 第57-58页 |
| ·规范化操作 | 第58页 |
| ·错误检测 | 第58-59页 |
| ·双链表的程序示例 | 第59-62页 |
| ·函数行为规范 | 第59-60页 |
| ·抽象化操作 | 第60-62页 |
| ·规范化操作 | 第62页 |
| ·调用C库函数的程序示例 | 第62-64页 |
| ·本章小结 | 第64-65页 |
| 第6章 实现及实验结果 | 第65-73页 |
| ·实现工作 | 第65-69页 |
| ·实验结果 | 第69-71页 |
| ·本章小结 | 第71-73页 |
| 第7章 结束语 | 第73-75页 |
| ·论文工作总结 | 第73-74页 |
| ·进一步研究方向 | 第74-75页 |
| 参考文献 | 第75-79页 |
| 致谢 | 第79-81页 |
| 在读期间发表的学术论文与取得的研究成果 | 第81页 |
