安全C语言验证器的形状系统的扩展设计与实现
| 摘要 | 第5-6页 |
| ABSTRACT | 第6-7页 |
| 第1章 绪论 | 第13-19页 |
| 1.1 研究背景 | 第13-14页 |
| 1.1.1 高可信软件 | 第13页 |
| 1.1.2 软件测试和形式验证 | 第13-14页 |
| 1.2 本文概述 | 第14-16页 |
| 1.2.1 本文工作 | 第14-15页 |
| 1.2.2 主要贡献 | 第15-16页 |
| 1.3 相关工作 | 第16页 |
| 1.4 本文章节安排 | 第16-19页 |
| 第2章 安全C语言验证器及形状系统简介 | 第19-27页 |
| 2.1 安全C语言验证器简介 | 第19-21页 |
| 2.2 形状系统简介 | 第21-24页 |
| 2.3 示例程序的演算分析 | 第24-26页 |
| 2.4 本章小结 | 第26-27页 |
| 第3章 形状系统演算的扩展实现 | 第27-43页 |
| 3.1 角标指针访问路径的节点定位演算 | 第27-34页 |
| 3.1.1 C风格指针访问路径的局限性 | 第27-28页 |
| 3.1.2 角标指针访问路径的概述 | 第28-29页 |
| 3.1.3 角标指针访问路径的节点定位演算详述 | 第29-34页 |
| 3.2 函数调用演算 | 第34-41页 |
| 3.2.1 函数调用演算概述 | 第34-36页 |
| 3.2.2 函数调用演算的窗口获取算法 | 第36-38页 |
| 3.2.3 函数调用演算的窗口合并算法 | 第38-41页 |
| 3.3 本章小结 | 第41-43页 |
| 第4章 形状系统的形状图构造方法改进 | 第43-55页 |
| 4.1 形状图精确构造方法 | 第43-51页 |
| 4.1.1 形状图精确构造方法概述 | 第43-44页 |
| 4.1.2 内置形状谓词阐述 | 第44-46页 |
| 4.1.3 形状图精确构造方法的操作语义 | 第46-49页 |
| 4.1.4 形状图精确构造方法的算法描述 | 第49-51页 |
| 4.2 自定义谓词的推断方法 | 第51-54页 |
| 4.2.1 自定义谓词推断方法概述 | 第51页 |
| 4.2.2 自定义谓词推断方法的算法描述 | 第51-54页 |
| 4.3 本章小结 | 第54-55页 |
| 第5章 形状系统的形状检查方法扩展 | 第55-67页 |
| 5.1 指针域标注概述 | 第55-56页 |
| 5.2 形状检查方法概述 | 第56-59页 |
| 5.2.1 形状级别概述 | 第56-57页 |
| 5.2.2 显式形状检查与隐式形状检查 | 第57-58页 |
| 5.2.3 形状检查方法的总体流程 | 第58-59页 |
| 5.3 形状检查方法三阶段处理详述 | 第59-66页 |
| 5.3.1 形状分割 | 第59-61页 |
| 5.3.2 形状分析 | 第61-64页 |
| 5.3.3 形状推断 | 第64-66页 |
| 5.4 本章小结 | 第66-67页 |
| 第6章 实验结果与实例分析 | 第67-75页 |
| 6.1 形状检查的实验结果及实例分析 | 第67-70页 |
| 6.1.1 形状检查的实验结果 | 第67-68页 |
| 6.1.2 形状检查的实例分析 | 第68-70页 |
| 6.2 形状系统的综合实验结果及实例解释 | 第70-73页 |
| 6.2.1 形状系统综合实验结果 | 第70-71页 |
| 6.2.2 综合实验的实例分析 | 第71-73页 |
| 6.3 本章小结 | 第73-75页 |
| 第7章 总结与进一步工作 | 第75-77页 |
| 7.1 工作总结 | 第75页 |
| 7.2 进一步工作 | 第75-77页 |
| 参考文献 | 第77-81页 |
| 附录A 内置形状谓词产生的形状图 | 第81-83页 |
| 致谢 | 第83-85页 |
| 在读期间发表的学术论文与取得的研究成果 | 第85页 |
