We present a framework for local interprocedural shape analysis that computes procedure summaries as transformers of procedure-local heaps (the parts of the heap that the procedure may reach). A main challenge in procedurelocal shape analysis is the handling of cutpoints, objects that separate the input heap of an invoked procedure from the rest of the heap, which - from the viewpoint of that invocation - is non-accessible and immutable. In this paper, we limit our attention to effectively cutpoint-free programs - programs in which the only objects that separate the callee's heap from the rest of the heap, when considering live reference fields, are the ones pointed to by the actual parameters of the invocation. This limitation (and certain variations of it, which we also describe) simplifies the local-reasoning about procedure calls because the analysis needs not track cutpoints. Furthermore, our analysis (conservatively) verifies that a program is effectively cutpoint-free, © Springer-Verlag Berlin Heidelberg 2013.
CITATION STYLE
Kreiker, J., Reps, T., Rinetzky, N., Sagiv, M., Wilhelm, R., & Yahav, E. (2013). Interprocedural shape analysis for effectively cutpoint-free programs. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 7797 LNCS, 414–445. https://doi.org/10.1007/978-3-642-37651-1_17
Mendeley helps you to discover research relevant for your work.