Model Checking C++ with Exceptions

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.

Authors: Petr Ročkai, Jiří Barnat, and Luboš Brim

Project: DIVINE4

Published in: Automated Verification of Critical Systems, 2014.

Go to pdf