Interprocedural analyses: a comparison

We present a framework for program analysis of languages with procedures wh ich is general enough to allow for a comparison of various approaches to in terprocedural analysis. Our framework is based on a small-step operational semantics and subsumes both frameworks for imperative and for logic languag es, We consider reachability analysis, that is, the problem of approximatin g the sets of program states reaching program points, We use our framework in order to clarify the impact of several independent design decisions on t he precision of the analysis, Thus, we compare intraprocedural forward accu mulation with intraprocedural backward accumulation, Furthermore, we consid er both relational and functional approaches, While for relational analysis the accumulation strategy makes no difference in precision, we prove for f unctional analysis that forward accumulation may lose precision against bac kward accumulation. Concerning the relative precision of relational analyse s and corresponding functional analyses, we exhibit scenarios where functio nal analysis does not lose precision, Finally, we explain why even an enhan cement of functional analysis through disjunctive completion of the underly ing abstract domain may sometimes lose precision against relational analysi s, (C) 2000 Elsevier Science Inc. All rights reserved.