Model checking C++ programs with exceptions
| Authors | |
|---|---|
| Year of publication | 2016 |
| Type | Article in Periodical |
| Magazine / Source | Science of Computer Programming |
| MU Faculty or unit | |
| Citation | |
| Web | http://dx.doi.org/10.1016/j.scico.2016.05.007 |
| Doi | http://dx.doi.org/10.1016/j.scico.2016.05.007 |
| 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: |