An Approach for Detecting Infeasible Paths Based on a SMT Solver

Software testing is an important means to ensure software quality. Testers need to ensure that every component of the software is tested correctly to achieve high coverage, such as path coverage, decision coverage, and branch coverage. An infeasible path is a path that cannot be traversed by any test cases. The existence of infeasible paths can waste test resources; therefore, detection of infeasible paths are necessary before path testing. This paper presents a static method for the detecting infeasible paths that is based on a satisfiability modulo theory (SMT) solver. First, the proposed method generates a sub-path set and converts the feasibility issues into inequalities. Second, a constraint solver is used to solve the inequalities and, then, the sub-paths are divided into two categories: infeasible sub-paths and undetermined sub-paths. The paths that were expanded from the latter will be tested again to determine their feasibility. Finally, the feasibility of all paths is detected. Most of the detection works are done on the sub-path set; therefore, our method provides an effective solution to the path-explosion problem. The experimental results showed that the proposed method can detect infeasible paths more accurately and effectively than most existing methods.