SMT-Based Refutation of Spurious Bug Reports in the Clang Static AnalyzerDemos
We describe and evaluate a bug refutation extension for the Clang Static Analyzer (CSA) that addresses the limitations of the existing built-in constraint solver. In particular, we complement CSA’s existing heuristics that remove spurious bug reports. We encode the path constraints produced by CSA as Satisfiability Modulo Theories (SMT) problems, use SMT solvers to precisely check them for satisfiability, and remove bug reports whose associated path constraints are unsatisfiable. Our refutation extension refutes spurious bug reports in 8 out of 12 widely used open-source applications; on average, it refutes ca. 7% of all bug reports, and never refutes any true bug report. It incurs only negligible performance overheads, and on average adds 1.2% to the runtime of the full Clang/LLVM toolchain. A demonstration is available at https://www.youtube.com/watch?v=ylW5iRYNsGA.
Wed 29 MayDisplayed time zone: Eastern Time (US & Canada) change
| 11:00 - 12:30 | Static AnalysisTechnical Track / Papers / Demonstrations at Viger Chair(s): Mauro Pezze Università della Svizzera italiana (USI) (Switzerland) and Università degli Studi di Milano Bicocca (Italy) | ||
| 11:0020m Talk | SMOKE: Scalable Path-Sensitive Memory Leak Detection for Millions of Lines of Code Technical Track Gang Fan Hong Kong University of Science and Technology, Rongxin Wu Department of Computer Science and Engineering, The Hong Kong University of Science and Technology, Qingkai Shi Hong Kong University of Science and Technology, Xiao Xiao Sourcebrella Inc., Jinguo Zhou Sourcebrella Inc., Charles Zhang The Hong Kong University of Science and TechnologyPre-print | ||
| 11:2020m Talk | Reasonably-Most-General Clients for JavaScript Library Analysis Technical Track | ||
| 11:4020m Talk | Resource-aware Program Analysis via Online Abstraction Coarsening Technical Track | ||
| 12:0020m Talk | SMT-Based Refutation of Spurious Bug Reports in the Clang Static AnalyzerDemos Demonstrations Mikhail R. Gadelha SIDIA Instituto de Ciência e Tecnologia, Enrico Steffinlongo , Lucas C. Cordeiro University of Manchester, UK, Bernd Fischer Stellenbosch University, Denis A. Nicole University of Southampton | ||
| 12:2010m Talk | Discussion Period Papers | ||



