Interprocedural shape analysis for cutpointfree programs

We present a framework for interprocedural shape analysis, which is context-and flow-sensitive with the ability to perform destructive pointer updates. We limit our attention to cutpoint-free programs—programs in which reasoning on a proce-dure call only requires consideration of context reachable from the actual param-eters. For such programs, we show that our framework is able to perform an effi-cient modular analysis. Technically, our analysis computes procedure summaries as transformers from inputs to outputs while ignoring parts of the heap not rele-vant to the procedure. This makes the analysis modular in the heap and thus allows reusing the effect of a procedure at different call-sites and even between different contexts occurring at the same call-site. We have implemented a prototype of our framework and used it to verify interesting properties of cutpoint-free programs