Generic Combination of Heap and Value Analyses in Abstract Interpretation

摘要: Abstract interpretation has been widely applied to approximate data structures and usually numerical value information. One needs combine them effectively apply static analysis real software. Nevertheless, they have studied mainly as orthogonal problems so far. In this context, we introduce a generic framework that, given heap analysis, combines them, formally prove its soundness. The approximates concrete locations with identifiers, that can be materialized or merged. Meanwhile, the tracks information both on variable taking into account when identifiers are merged materialized. We show how existing pointer shape analyses, well domains, plugged in our framework. As far know, is first sound automatic combining analyses allows freely manage identifiers.