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.