2015/10/27 by Kamil Dudka, Dudka, Kamil, Lukáš Holík +7
Computer Science · #FOS: Computer and information sciences #Logic, programming, and type systems #Parallel Computing and Optimization Techniques #Programming Languages (cs.PL) #Software Engineering Research
paper · pdf · doi:10.48550/arxiv.1510.07995
openalex publication_date 2015/10/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 pushback or popfront. 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.