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.