$ show esbmc/esbmc
ESBMC (Efficient SMT-based Bounded Model Checker) is a mature, open-source formal verification tool that automatically detects or proves the absence of runtime errors in C, C++, Python, Java/Kotlin (via Jimple), CHERI, and Solidity programs. It parses source code using language-specific frontends (Clang for C/C++, CPython parser for Python, Soot for Java), converts programs into a common GOTO intermediate representation, and performs bounded symbolic execution with SMT solving (Z3, Bitwuzla, CVC5, Yices, etc.). The tool checks for assertions, memory safety (buffer overflows, null pointers, use-after-free), arithmetic overflows, concurrency races, and user-defined contracts (requires/ensures/assigns). It supports advanced verification techniques including k-induction, loop invariant synthesis, incremental BMC, and quantifier reasoning. The architecture is modular: frontends produce GOTO programs, which are then processed by a series of analysis passes (pointer analysis, value-set analysis, loop unrolling, contract enforcement) before being encoded into SMT formulas. The solver backend is pluggable, with support for interactive solvers and experimental one-shot solvers (Mallob, NeuroSym). The repository includes an extensive regression test suite with thousands of small, self-contained test cases organized by language and feature, many with paired passing/failing variants to ensure soundness. Operational models for C standard library functions, C++ STL, Python standard library (including numpy), and SystemC are bundled as source code for SMT translation. Key entry points include the main ESBMC binary (built from `src/esbmc/`), the Clang C/C++ frontend (`src/clang-c-frontend/`), the Python frontend (`src/python-frontend/`), and the solver interfaces (`src/solvers/`). The tool is actively used in research and industry, has won 43 awards at SV-COMP and Test-Comp, and is supported by multiple funding agencies. External dependencies include Boost (program_options, filesystem), Clang/LLVM, and several SMT solvers.
The LLM identified 6 files worth highlighting for reuse:
Provides simple, header-only functions `has_prefix` and `has_suffix` for checking string prefixes and suffixes. No internal dependencies, can be extracted into any C++ project needing these predicates.
Implements the `__VERIFIER_nondet_*` family of functions (nondet_int, nondet_bool, nondet_float, etc.) used by SV-COMP benchmarks and ESBMC's own tests. This is a standalone C file that models nondeterministic input generation for verification. Reusable by any verification tool that follows the SV-COMP convention.
Operational model for `setjmp`/`longjmp` that captures the non-local jump semantics for SMT-based verification. Self-contained C source that can be reused in other bounded model checkers needing setjmp/longjmp support.
Operational model for numpy linear algebra functions (e.g., `norm`, `det`, `inv`, `solve`) written in pure Python. Designed to be used by ESBMC's Python frontend for symbolic execution of numpy code. Could be extracted and adapted for other Python verification tools that need numpy semantics.
Portable header that provides `char16_t`, `char32_t`, and related `<uchar.h>` functionality for C++ environments where the standard header is missing. Self-contained and reusable for cross-platform C++ projects.
Provides symbol renaming utilities to avoid name collisions during program transformation. Implements a simple counter-based renaming scheme. Could be extracted for any tool that needs to generate unique identifiers.