A Fast and Precise Static Loop Analysis Based on Abstract Interpretation, Program Slicing and Polytope Models