Wednesday, June 10, 2015
Speaker: Tomáš Vojnar
Venue: TU Wien
Time: 16:00. Day: Wednesday. Room: Lecture hall EI2, Gußhausstraße 25, 2.Stock, Stiege VIII
We propose a method that transforms a C program manipulating lists via low-level pointer statements into an equivalent program where the lists are manipulated via calls of standard high-level container operations like push_back, pop_front, etc. 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. The resulting program where low-level pointer statements are summarized into high-level container operations is more understandable and better suitable for program analyses since the burden of analysing low-level pointer manipulations gets removed. We have implemented our approach and successfully tested it through a number of experiments, including experiments showing that our method can indeed be used to ease program analysis by separating shape analysis from analysing data-related properties. The result is a joint work with Kamil Dudka, Lukas Holik, and Petr Peringer from Brno University of Technology and Marek Trtik from Verimag, Grenoble.