Skip to content
Documentation
C and C++

C and C++

C and C++ are ESBMC’s primary frontends, built on Clang/LLVM. ESBMC verifies C (up to C23) and C++ (up to C++20, with selected C++23 features), checking memory safety, arithmetic overflow, pointer safety, concurrency properties, and user assertions — or proving their absence.

To get started, see the Usage guide and the Constructs reference for the verification annotations. The pages below cover C/C++-specific tooling and support.

C++ Support
Which C++ language and STL features ESBMC supports.
C++ Workflow and Resources
A practical workflow and resources for verifying C++ programs.
CTest Test Generation
Materialise reached witnesses as runnable CTest cases.
HTML Report Generation
Generate browsable HTML reports of verification results.
Reducing C Programs
Shrink a failing C program to a minimal reproducer.