Tomas Vojnar
From Pointers to List Containers
RiSE will host a talk by Tomas Vojnar on June 10, 2015.
DATE: | Wednesday, June 10, 2015 |
TIME: | 16:00 |
VENUE: | Lecture hall EI2, Gußhausstraße 25, 2.Stock, Stiege VIII |
CONTACT
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.