Reconstructing Paths for Reachable Code.

Infeasible code has proved to be an interesting target for static analysis. It allows modular and scalable analysis, and at the same time, can be implemented with a close-to-zero rate of false warnings. The challenge for an infeasible code detection algorithm is to find executions that cover all statements with feasible executions as fast as possible. The remaining statements are infeasible code. In this paper we propose a new encoding of programs into first-order logic formulas that allows us to query the non-existence of feasible executions of a program, and, to reconstruct a feasible path from counterexamples produced for this query. We use these paths to develop a path-cover algorithm based on blocking clauses. We evaluate our approach using several real-world applications and show that our new prover-friendly encoding yields a significant speed-up over existing approaches.