SMT-constrained symbolic execution for eclipse CDT/Codan

Abstract

This paper presents a symbolic execution plug-in extension for Eclipse CDT/Codan, which serves to reason about satisfiable paths of C programs. Programs are translated into the SMT-LIB sublogic of arrays, uninterpreted functions and nonlinear integer and real arithmetic (AUFNIRA), and path satisfiability is automatically examined with an SMT solver. The presented plug-in can serve as a basis for path-sensitive static bug detection with bounded or unrestricted context, where the presence of bugs is decided with the solver. An interface provides notifications and context information for checker classes. With a buffer bound checker the symbolic execution plug-in is shown capable of accurately detecting bugs with currently 36 of the 39 C flow variants of the NSA's Juliet test suite for static analyzers. © 2014 Springer International Publishing.