ESBMC v7.6: Enhanced Model Checking of C++ Programs with Clang AST

TL;DR

ESBMC v7.6 advances model checking for modern C++ programs by integrating Clang AST features, enabling verification of complex C++ features like exceptions, memory safety, and STL operations.

Contribution

This work extends ESBMC with new Clang AST-based features, improving support for modern C++ constructs and enhancing verification capabilities.

Findings

Handles a broader range of C++ features

Verifies memory safety issues effectively

Supports recent C++ standard features

Abstract

This paper presents Efficient SMT-Based Context-Bounded Model Checker (ESBMC) v7.6, an extended version based on previous work on ESBMC v7.3 by K. Song et al. The v7.3 introduced a new Clang-based C++ front-end to address the challenges posed by modern C++ programs. Although the new front-end has demonstrated significant potential in previous studies, it remains in the developmental stage and lacks several essential features. ESBMC v7.6 further enhanced this foundation by adding and extending features based on the Clang AST, such as 1) exception handling, 2) extended memory management and memory safety verification, including dangling pointers, duplicate deallocation, memory leaks and rvalue references and 3) new operational models for STL updating the outdated C++ operational models. Our extensive experiments demonstrate that ESBMC v7.6 can handle a significantly broader range of C++ features introduced in recent versions of the C++ standard.