Efficient detection and exploitation of infeasible paths for software timing analysis