So we do whole program analysis. We start at the first statement in
global scope, model it, then add all its successor to a queue, and
keep modelling until we get to the end of the program. When we get to
a method call, we start modelling the execution of the method. At the
end of the method, we propagate the results back to the caller, model
the return value, and carry on modelling the caller.
it sounds like this algorithm:
Precise interprocedural dataflow analysis via graph reachability, POPL'95
http://portal.acm.org/citation.cfm?id=199462
Nuno