Publication Details

From Low-Level Pointers to High-Level Containers, Technical Report No. FIT-TR-2015-03

DUDKA Kamil, HOLÍK Lukáš, PERINGER Petr, TRTÍK Marek and VOJNAR Tomáš. From Low-Level Pointers to High-Level Containers, Technical Report No. FIT-TR-2015-03. Brno, 2016. Available from: http://arxiv.org/pdf/1510.07995v1.pdf
Type
technical report
Language
english
Authors
Dudka Kamil, Ing. (DITS FIT BUT)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Peringer Petr, Dr. Ing. (DITS FIT BUT)
Trtík Marek, Mgr., Ph.D. (FI MUNI)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
URL
Annotation

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.

Published
2016
Pages
1-28
Place
Brno, CZ
BibTeX 
@TECHREPORT{FITPUB11061,
   author = "Kamil Dudka and Luk\'{a}\v{s} Hol\'{i}k and Petr Peringer and Marek Trt\'{i}k and Tom\'{a}\v{s} Vojnar",
   title = "From Low-Level Pointers to High-Level Containers, Technical Report No. FIT-TR-2015-03",
   pages = "1--28",
   year = 2016,
   location = "Brno, CZ",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/11061"
}
Back to top