Model checking C++ programs with exceptions

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

ROČKAI Petr BARNAT Jiří BRIM Luboš

Year of publication 2016
Type Article in Periodical
Magazine / Source Science of Computer Programming
MU Faculty or unit

Faculty of Informatics

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:

You are running an old browser version. We recommend updating your browser to its latest version.