C语言类别的指向分析的定义和实现
摘要：指针问题是确定指针变量可能的运行时目标的问题，并且通常被认为是更一般的别名问题的一部分，该问题是确定不同表达式是否以及何时可以引用相同的内存地址。别名信息对于需要推理程序语义的每个工具都是必不可少的。然而，由于众所周知的不可判定结果，对于允许别名的所有有趣的语言来说，非平凡别名问题的确切解决方案通常是不可计算的。这项工作集中于通过提出一种基于存储的、流敏感的指针分析方法来近似解决这个问题，应用于自动化软件验证领域。与启发式地对程序针对有限执行集进行检查的软件测试过程不同，本文所考虑的方法是静态分析，所计算的结果对所有可能的分析程序的执行都是有效的。我们介绍了一种简化的编程语言及其执行模型；然后使用抽象解释理论的思想，发展了一种近似的执行模型。最后，形式上证明了近似性的正确性。通过对初始简化模型进行扩展并讨论其表述的正确性，追求开发一个实际的指针分析。本工作还对指针分析问题做出了原创性贡献，提供了一个关于指针抽象域的过滤操作的表述，并对定义的抽象操作的正确性进行了正式证明；就我们所知，这些内容在先前的文献中尚未提及。
作者：Stefano Soffia
论文ID：0810.0753
分类：Programming Languages
分类简称：cs.PL
提交时间：2008-10-07