C++ Support

This page is a reference of the C++ language features and standard-library headers supported by ESBMC’s Clang-based C++ frontend. For what is not supported, see Limitations.

At a glance

The default is C++17. Select a different standard with --std, for example --std c++20 or --std c++03.

Support is not gap-free at any standard — see Limitations for the known exceptions, notably constructor and destructor ordering.

Verifying a C++ program

ESBMC checks memory safety, arithmetic overflow, pointer safety and user assertions across all inputs, rather than the single input a test would exercise. Given shape.cpp:

#include <cassert>

class Shape
{
public:
  virtual int area() const = 0;
  virtual ~Shape() = default;
};

class Square : public Shape
{
  int side;

public:
  Square(int s) : side(s) {}
  int area() const override { return side * side; }
};

int main()
{
  int n = nondet_int();
  __ESBMC_assume(n >= 1 && n < 100);

  Shape *s = new Square(n);
  assert(s->area() > n);
  delete s;
  return 0;
}

Run it with:

esbmc shape.cpp --incremental-bmc

ESBMC finds the one input that breaks the assertion — n == 1, where 1 * 1 is not greater than 1:

[Counterexample]

State 1 file shape.cpp line 21 column 3 function main thread 0
----------------------------------------------------
  n = 1 (00000000 00000000 00000000 00000001)

State 5 file shape.cpp line 25 column 3 function main thread 0
----------------------------------------------------
Violated property:
  file shape.cpp line 25 column 3 function main
  assertion main
  !((_Bool)((signed long int)(!(return_value$ > n))))

VERIFICATION FAILED

Tightening the assumption to n > 1 makes the property hold for every one of the remaining inputs, and ESBMC reports VERIFICATION SUCCESSFUL.

See the Usage guide for the full set of options and the Constructs reference for __ESBMC_assume, nondet_int and the other verification annotations.

Operational models vs. host headers

By default ESBMC compiles C++ with -nostdinc++, so #include <vector> resolves to ESBMC’s own operational model (OM) rather than your host standard library. OMs are written to be verification-friendly — small, loop-free where possible, and free of the inline assembly and compiler intrinsics that real standard-library implementations rely on.

Two flags change this behaviour:

--mix-cpp-host-headers is the escape hatch for a header ESBMC does not model (see Not modelled below). It is opt-in because names defined by both the OMs and the host library — char_traits, istream and similar — can then produce ambiguity errors at parse time.

Language features

Classes and objects

• Classes, member functions, member access control
• Constructors and destructors, including default, copy and move forms
• Static and non-static data members; default member initialisers
• Unions, including anonymous unions
• typeid on a polymorphic glvalue reports the dynamic type, and the type_info name string is NUL-terminated

Constructors and destructors

• Delegating and inheriting constructors (using Base::Base;), including multi-base and chained forms
• Virtual bases are initialised only in the most-derived constructor
• Destructor chains for members and bases, including virtual base destructors
• Destructors run on return paths, for discarded results, and for temporaries destroyed mid-expression

References, temporaries and move semantics

• Lvalue and rvalue references
• Move constructors and move assignment operators
• Address-of distributes over a conditional lvalue; class-typed conditionals elide their temporaries; a reference parameter binds to the selected arm

Templates

• Class and function templates, partial and explicit specialisation
• Variable templates (C++14) and variable template declarations (C++17)
• Class template argument deduction (CTAD)
• Concepts and requires clauses (C++20)

Inheritance and polymorphism

• Single-level and multi-level polymorphism
• Pure virtual methods and abstract classes
• Virtual inheritance, including the diamond problem
• Multiple inheritance: nested base subobjects, dynamic_cast<T*> re-offsetting across bases, override thunks keyed by each base’s virtual name and adjusted by the indirect base’s cumulative offset, and catch-by-base binding re-offset for multiple-inheritance thrown types
• Virtual dispatch through a non-arrow member expression — (*p).f() and ref.f() dispatch virtually

Memory management

• new / delete and new[] / delete[]
• Detection of dangling pointers, double delete and mismatched operators
• Placement new, including the form without an initialiser
• delete dispatches through the virtual destructor slot; deleting through a base subobject whose destructor is not virtual is rejected

Exceptions

try / catch / throw are supported directly. Passing --lower-exceptions additionally lowers exception handling into explicit control flow, which enables:

• noexcept and throw() exception specifications
• Dynamic exception specifications, with unexpected / bad_exception recovery
• std::exception_ptr with current_exception, rethrow_exception and make_exception_ptr, plus nested exceptions (throw_with_nested, rethrow_if_nested)
• std::uncaught_exception / std::uncaught_exceptions, via a lowered per-thread count

Other exception behaviour:

• dynamic_cast<T&> throws std::bad_cast on a failed reference cast
• std::vector::at and std::string::at throw std::out_of_range rather than asserting
• std::bad_cast and std::bad_typeid derive from std::exception with a virtual what()
• The exception-state globals are thread-local, so each thread raises, catches and clears its own in-flight exception independently; concurrently-throwing programs are lowered rather than rejected

Selected C++17 / C++20 / C++23 features

Standard-library coverage

The headers below are modelled by ESBMC’s own operational models and are covered by regression tests under regression/esbmc-cpp*.

Containers and iterators

std::multimap and std::multiset track std::map and std::set, including contains and cbegin/cend.

Strings and streams

Utilities and type support

Algorithms and numerics

Concurrency

<thread>, <mutex> and <condition_variable> are lowered onto ESBMC’s pthread model, so interleaving exploration, deadlock detection and data-race detection apply to std::thread programs. std::promise and std::future are modelled on the same basis, and <atomic> is modelled with atomic sections.

C library headers

<cassert>, <cctype>, <cerrno>, <cfloat>, <ciso646>, <climits>, <clocale>, <cmath>, <csetjmp>, <csignal>, <cstdarg>, <cstddef>, <cstdint>, <cstdio>, <cstdlib>, <cstring> and <ctime> are available.

Standard-version guards

<compare> is includable before C++20; <bit>, <span> and <expected> are guarded by standard version; <array> is usable in C++11; <limits> works under --std c++11 and c++14; and the C++98 container headers parse under --std c++03.

Not modelled

The following standard headers have no operational model. Including one either fails to resolve, or falls through to your host header under --mix-cpp-host-headers — in which case ESBMC has to verify the real implementation, which is frequently intractable.

<forward_list>, <regex>, <ranges>, <format>, <concepts>, <coroutine>, <charconv>, <numbers>, <ratio>, <typeindex>, <shared_mutex>, <barrier>, <latch>, <semaphore>, <stop_token>, <syncstream>, <execution>, <memory_resource>, <scoped_allocator>, <cwchar>, <cwctype>, <cfenv>, <cinttypes>.

Note that <concepts> being unmodelled does not affect the language feature — concepts and requires clauses are supported, as listed above.

Current status

Feature support is tracked on the issue tracker under the C++ label. For the current pass rate, run the esbmc-cpp* regression suites or consult the CI results.

Maintainers: see C++ Workflow and Resources for benchmark tracking and the development workflow.