Model checking C++ programs with exceptions

Logo poskytovatele

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

ROČKAI Petr BARNAT Jiří BRIM Luboš

Rok publikování 2016
Druh Článek v odborném periodiku
Časopis / Zdroj Science of Computer Programming
Fakulta / Pracoviště MU

Fakulta informatiky

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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.