A semantical framework for practical program flow analysis