Model checking C++ programs with exceptions

•Description of the translation of C++ exceptions to LLVM exceptions.•Detailed description of exception handling in LLVM.•An extension of the explicit-state model checker DIVINE to handle LLVM exceptions.•A summary of applications for the extended model checker.

We present an extension of the DIVINE software model checker to support programs with exception handling. The extension consists of two parts, a language-neutral implementation of the LLVM exception-handling instructions, and an adaptation of the C++ runtime for the DIVINE/LLVM exception model. This constitutes an important step towards support of both the full C++ specification and towards verification of real-world C++ programs using a software model checker. Additionally, we show how these extensions can be used to elegantly implement other features with non-local control transfer, most importantly the longjmp function in C.