Result Details
From Low-Level Pointers to High-Level Containers, Technical Report No. FIT-TR-2015-03
Holík Lukáš, doc. Mgr., Ph.D., DITS (FIT)
Peringer Petr, Dr. Ing., DITS (FIT)
Trtík Marek
Vojnar Tomáš, prof. Ing., Ph.D., DITS (FIT)
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 since the burden of dealing with low-level pointer manipulations gets removed. 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.
@misc{BUT168641,
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, Technical Report No. FIT-TR-2015-03",
year="2016",
pages="1--28",
address="Brno",
url="http://arxiv.org/pdf/1510.07995v1.pdf"
}