A generic framework for heap and value analyses of object-oriented programming languages

Abstract interpretation has been widely applied to approximate data structures and (usually numerical) value information, but their combination is needed to effectively apply static analysis to real software. In this context, we introduce a generic framework that, given a heap and a value analysis, combines them, proving formally its soundness. We plug inside this framework a standard allocation site-based pointer analysis, a TVLA-based shape analysis, and standard existing numerical domains. As far as we know, this is the first sound generic automatic framework for statically typed object-oriented programming languages combining heap and value analyses that allows to summarize and materialize heap identifiers.