从低级指针到高级容器
编程语言
2015-10-28 v1
摘要
我们提出一种方法，将使用低级指针语句操纵容器的C程序转换为等价程序，其中容器通过调用标准高级容器操作如push_back或pop_front来操纵。我们方法的输入是一个用特殊形式形状不变式标注的C程序，该不变式可在稍作修改后从当前自动形状分析器获得。所得程序将低级指针语句概括为高级容器操作，更易理解且(除其他可能的好处外)更适于程序分析。我们已实现我们的方法并通过若干基于链表的容器实验成功测试，包括通过分离形状分析与数据相关属性分析来简化程序分析的实验。
引用
@article{arxiv.1510.07995,
title = {From Low-Level Pointers to High-Level Containers},
author = {Kamil Dudka and Lukáš Holík and Petr Peringer and Marek Trtík and Tomáš Vojnar},
journal= {arXiv preprint arXiv:1510.07995},
year = {2015}
}
备注
An extended version of a VMCAI'16 paper