  An important step toward adoption of formal methods in software development
is support for mainstream programming languages. Unfortunately, these languages
are often rather complex and come with substantial standard libraries. However,
by choosing a suitable intermediate language, most of the complexity can be
delegated to existing execution-oriented (as opposed to verification-oriented)
compiler frontends and standard library implementations. In this paper, we
describe how support for C++ exceptions can take advantage of the same
principle. Our work is based on DiVM, an LLVM-derived, verification-friendly
intermediate language.
  Our implementation consists of 2 parts: an implementation of the `libunwind`
platform API which is linked to the program under test and consists of 9 C
functions. The other part is a preprocessor for LLVM bitcode which prepares
exception-related metadata and replaces associated special-purpose LLVM
instructions.
