Publication Details
From Low-Level Pointers to High-Level Containers
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Peringer Petr, Dr. Ing. (DITS)
Trtík Marek (FIT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
program analysis, static analysis, shape analysis, heap abstraction, symbolic memory graphs, program transformation, pointer programs, container programs
We propose a method that transforms a C program manipulating containers using low-level pointer statements into an equivalent program where the containers are manipulated via calls of standard high-level container operations like push_back or pop_front. The input of our method is a C program annotated by a special form of shape invariants which can be obtained from current automatic shape analysers after a slight modification. The resulting program where the low-level pointer statements are summarized into high-level container operations is more understandable and (among other possible benefits) better suitable for program analysis. We have implemented our approach and successfully tested it through a number of experiments with list-based containers, including experiments with simplification of program analysis by separating shape analysis from analysing data-related properties.
@inproceedings{BUT130929,
author="Kamil {Dudka} and Lukáš {Holík} and Petr {Peringer} and Marek {Trtík} and Tomáš {Vojnar}",
title="From Low-Level Pointers to High-Level Containers",
booktitle="Verification, Model Checking, and Abstract Interpretation (VMCAI)",
year="2016",
series="Lecture Notes in Computer Science",
volume="9583",
pages="431--452",
publisher="Springer Verlag",
address="Berlin Heidelberg",
doi="10.1007/978-3-662-49122-5\{_}21",
isbn="978-3-662-49121-8",
url="http://www.springer.com/la/book/9783662491218"
}