The Interprocedural Coincidence Theorem
J. Knoop, B. Steffen
We present an interprocedural generalization of the well-known
(intraprocedural) Coincidence Theorem of Kam and Ullman,
which provides a sufficient condition for the equivalence
of the {\em meet over all paths} (MOP) solution and the {\em
maximal fixed point} (MFP) solution to a data flow analysis
problem. This generalization covers arbitrary imperative
programs with recursive procedures, formal parameters and
local variables, and, in the absence of procedures, reduces
to the classical intraprocedural version. In particular,
our stack-based approach generalizes the coincidence theorems
of Barth and Sharir-Pnueli for the same setup, which do not
properly deal with local variables of recursive procedures.