Support for KLEE in Debile

Writing and maintaining software is challenging. Software is complex and keeping it bug-free remains an unsolved problem. Debian Stretch, the next Debian stable release, comprises 850 million lines of software source code. Code written in the C programming language accounts for 41% of the lines, which is more than in any other programming language. Debile, Debian’s package analysis platform, so far includes the CppCheck, Clang Static Analyzer, and Coccinelle tools for packages with C, C++, and Objective-C code. However, all of the tools perform static analyses, which can result in false positives. Too many reported false positives hinder adoption of the tools. To address this issue, I propose to integrate the KLEE tool into Debile. KLEE performs dynamic analysis on C programs and reports only true positives, i.e. real bugs. It does so by systematically exploring as many as possible execution paths in a given program. Errors that KLEE reports exist only along feasible execution paths, i.e. they correspond to real bugs in the program.