Model Checking C++ with Exceptions
Abstract
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.
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.
Full Text:
PDFDOI: http://dx.doi.org/10.14279/tuj.eceasst.70.983
DOI (PDF): http://dx.doi.org/10.14279/tuj.eceasst.70.983.962
Hosted By Universitätsbibliothek TU Berlin.