Model checking C++ programs with exceptions
| Autoři | |
|---|---|
| Rok publikování | 2016 |
| Druh | Článek v odborném periodiku |
| Časopis / Zdroj | Science of Computer Programming |
| Fakulta / Pracoviště MU | |
| Citace | |
| www | http://dx.doi.org/10.1016/j.scico.2016.05.007 |
| Doi | http://dx.doi.org/10.1016/j.scico.2016.05.007 |
| Obor | Informatika |
| Klíčová slova | Model checking; C++; Exception handling; LLVM |
| Popis | 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. |
| Související projekty: |