Model checking C++ programs with exceptions

Logo poskytovatele

Varování

Publikace nespadá pod Ekonomicko-správní 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.