Informace o publikaci
From Low-Level Pointers to High-Level Containers
| Autoři | |
|---|---|
| Rok publikování | 2016 |
| Druh | Článek ve sborníku |
| Konference | Verification, Model Checking, and Abstract Interpretation |
| Fakulta / Pracoviště MU | |
| Citace | |
| Doi | http://dx.doi.org/10.1007/978-3-662-49122-5_21 |
| Obor | Počítačový hardware a software |
| Klíčová slova | Shape analysis; list; program transformation |
| Popis | 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. |