Publication details
Model Checking C++ with Exceptions
| Authors | |
|---|---|
| Year of publication | 2014 |
| Type | Article in Periodical |
| Magazine / Source | Electronic Communications of the EASST |
| MU Faculty or unit | |
| Citation | |
| Web | http://journal.ub.tu-berlin.de/eceasst/article/view/983 |
| Doi | http://dx.doi.org/10.14279/tuj.eceasst.70.983 |
| Field | Informatics |
| Keywords | model checking; C++ exception handling; LLVM |
| Description | 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. |
| Related projects: |