Build Guide

TLDR

Ubuntu 24.04

To compile ESBMC on Ubuntu 24.04 with LLVM 14 and the SMT solver Z3:

sudo apt update
sudo apt-get install -y clang-14 llvm-14 clang-tidy-14 python-is-python3 python3 git ccache unzip wget curl bison flex g++-multilib linux-libc-dev libboost-all-dev libz3-dev libclang-14-dev libclang-cpp-dev cmake
git clone https://github.com/esbmc/esbmc.git
cd esbmc
mkdir build && cd build
cmake .. -DENABLE_Z3=1
make -j4

To enable Python frontend support, add the -DENABLE_PYTHON_FRONTEND=1 flag to the cmake command and ensure you have Python 3 with the ast2json module installed:

pip install ast2json
cmake .. -DENABLE_Z3=1 -DENABLE_PYTHON_FRONTEND=1
make -j4

Fedora 40

To compile ESBMC on Fedora 40 with the latest version of LLVM and the SMT solver Z3:

# Warning, the --allowerasing parameter will also remove incompatible packages to the packages specified below
sudo dnf install --best --allowerasing "@Development Tools" clang llvm llvm-devel clang-tools-extra python3 git ccache unzip wget curl bison flex gcc-c++ glibc-devel glibc-devel.i686 boost-devel boost-devel.i686 z3-devel clang-devel clang-devel.i686 cmake zlib-devel libffi-devel libstdc++-devel libstdc++-devel.i686
git clone https://github.com/esbmc/esbmc.git
cd esbmc
mkdir build && cd build
CXX=g++ CC=gcc cmake .. -DENABLE_Z3=1 -DBUILD_TESTING=On -DENABLE_REGRESSION=1 -DZ3_DIR=/usr/include/z3
make -j4

To build ESBMC with other operating systems and SMT solvers, please see the BUILDING file.

FreeBSD

ESBMC should compile just fine in FreeBSD as long as the 32-bit libraries are enabled

pkg install git cmake python3 z3 bison flex boost-all
wget https://github.com/llvm/llvm-project/releases/download/llvmorg-16.0.0/clang+llvm-16.0.0-amd64-unknown-freebsd13.tar.xz && mv clang16
mkdir build && cd build
cmake .. -DLLVM_DIR=../clang16 -DClang_DIR=../clang16
make -j4

Mac OS X

M1/M2/M3/M4 Macs are now supported.

Given the elements of OS X, run the script. It runs on both ARM and Intel macs. You do need Homebrew installed. It creates the build folder, installs the Boolector SMT solver, and makes esbmc available globally. The script also supports building the Python frontend. Note that the Python frontend is quite early in its support for Python.

 ./build-esbmc-mac.sh

The raw command is provided here for your reference.

cmake .. -DZ3_DIR=/opt/homebrew/Cellar/z3/4.13.4 -DENABLE_Z3=1 -DC2GOTO_SYSROOT=/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk -DLLVM_DIR=/opt/homebrew/opt/llvm/lib/cmake/llvm -DClang_DIR=/opt/homebrew/opt/llvm/lib/cmake/clang
make -j8
make install

Details

This guide provides instructions on building ESBMC and its supported solvers.

It has been tested with Ubuntu 20.04.1, Ubuntu 22.04 and macOS Catalina as well as Windows 10 WSL v1 or v2 Ubuntu WSL, but the steps are mostly the same for other Linux and macOS distributions.

It is recommended that the RAM should be at least 6 GB.

Before starting, note that ESBMC is mainly distributed under the terms of the Apache License 2.0, so please read it carefully.

Dependency overview

The version requirements are stable but can change between releases.

Installing build tools and basic dependencies

We need to install some dependencies before moving into the next steps.

All of them are listed in the following installation command:

Linux:
sudo apt-get update && sudo apt-get install build-essential git gperf libgmp-dev cmake bison curl flex g++-multilib linux-libc-dev libboost-all-dev libtinfo-dev ninja-build python3-setuptools unzip wget python3-pip openjdk-8-jre

macOS:
brew install gmp cmake boost ninja python3 wget automake flex bison && pip3 install PySMT

Note that the packages are listed with their name in Debian/Ubuntu, but they can be found in other distributions as well.

Cloning ESBMC Source Code

ESBMC source code is publicly available in Github.

Before cloning the ESBMC Source Code, it is better to make a directory to contain the whole project in “ESBMC_Project”.

You can get the latest version using the following git command:

mkdir ESBMC_Project && cd ESBMC_Project && git clone https://github.com/esbmc/esbmc

Preparing Clang

Here, you have a choice: either build against the standard LLVM/Clang as distributed by the developers or the distribution, or to use a CHERI-enabled LLVM/Clang toolchain for ESBMC’s frontend in case you want to verify CHERI-C programs as well. Note that the CHERI-support in ESBMC is experimental and incomplete at this point.

If you are building ESBMC-CHERI, skip the following sections and go straight to Section Preparing CHERI Clang 13 (experimental).

Preparing external standard Clang 21 (recommended for a static build)

You can either download and unpack a release manually:

wget https://github.com/esbmc/esbmc/releases/download/v7.10/clang+llvm-21.1.2-x86_64-linux-gnu-ubuntu-22.04.tar.xz && tar xfJ clang+llvm-21.1.2-x86_64-linux-gnu-ubuntu-22.04.tar.xz &&
ESBMC_CLANG=$(echo -D{LLVM,Clang}_DIR=$PWD/clang+llvm-21.1.2-x86_64-linux-gnu-ubuntu-22.04) &&
ESBMC_STATIC=ON

or use ESBMC’s default for downloading dependencies during the build process:

ESBMC_CLANG=-DDOWNLOAD_DEPENDENCIES=ON
ESBMC_STATIC=ON

We’ll use these variables later in the build process. Note that downloading dependencies work for most of the dependencies covered below as well. In this case, you can directly jump to the section “Building ESBMC”. Remember that it is optional to keep all the features enabled. They are optional.

Preparing distributed Clang 16 (recommended for a shared build)

For shared builds, it is recommended to use the system’s LLVM/Clang, which on Ubuntu 24.04 can be obtained by:

apt-get install libclang-cpp16-dev &&
ESBMC_CLANG="-DLLVM_DIR=/usr/lib/llvm-16/lib/cmake/llvm -DClang_DIR=/usr/lib/cmake/clang-16" &&
ESBMC_STATIC=OFF

Preparing CHERI Clang 13 (experimental)

CHERI-enabled ESBMC uses CHERI clang in its front-end. It currently supports the release 20210817 based on clang version 13.0.0.

First, we need to download the package. It can be performed using the following wget command:

wget https://github.com/CTSRD-CHERI/llvm-project/archive/refs/tags/cheri-rel-20210817.tar.gz

Before build the package, check that lld is installed:

sudo apt-get install lld

Then, we need to extract and build the package. You can use the following commands:

tar xf cheri-rel-20210817.tar.gz &&
mkdir clang13 &&
cd llvm-project-cheri-rel-20210817 &&
mkdir build &&
cd build &&
cmake -GNinja -S ../llvm -DCMAKE_BUILD_TYPE=Release -DLLVM_PARALLEL_LINK_JOBS=4 -DLLVM_CCACHE_BUILD=FALSE -DLLVM_INSTALL_BINUTILS_SYMLINKS=TRUE -DLLVM_ENABLE_LIBXML2=FALSE -DLLVM_ENABLE_ZLIB=FALSE -DLLVM_ENABLE_OCAMLDOC=FALSE -DLLVM_ENABLE_BINDINGS=FALSE -DLLVM_INCLUDE_EXAMPLES=FALSE -DLLVM_INCLUDE_DOCS=FALSE -DLLVM_INCLUDE_BENCHMARKS=FALSE -DCLANG_ENABLE_STATIC_ANALYZER=FALSE -DCLANG_ENABLE_ARCMT=FALSE -DLLVM_ENABLE_Z3_SOLVER=FALSE -DLLVM_TOOL_LLVM_MCA_BUILD=FALSE -DLLVM_TOOL_LLVM_EXEGESIS_BUILD=FALSE -DLLVM_TOOL_LLVM_RC_BUILD=FALSE -DLLVM_OPTIMIZED_TABLEGEN=FALSE -DLLVM_USE_SPLIT_DWARF=TRUE -DLLVM_ENABLE_ASSERTIONS=TRUE '-DLLVM_LIT_ARGS=--max-time 3600 --timeout 300 -s -vv' '-DLLVM_TARGETS_TO_BUILD=AArch64;ARM;Mips;RISCV;X86;host' -DENABLE_EXPERIMENTAL_NEW_PASS_MANAGER=FALSE -DCLANG_ROUND_TRIP_CC1_ARGS=FALSE '-DLLVM_ENABLE_PROJECTS=llvm;clang' -DCMAKE_INSTALL_PREFIX=../../clang13 -DCMAKE_C_COMPILER=/usr/bin/cc -DCMAKE_CXX_COMPILER=/usr/bin/c++ -DCMAKE_ASM_COMPILER=/usr/bin/cc -DCMAKE_BUILD_RPATH_USE_ORIGIN=TRUE
ninja &&
ninja install &&
cd ../.. &&
ESBMC_CLANG=$(echo -D{LLVM,Clang}_DIR=$PWD/clang13) &&
ESBMC_STATIC=Off

Preparing the Solidity frontend (optional)

We developed a Solidity frontend for the efficient SMT-based context-bounded model checker (ESBMC). ESBMC-solidity is a permissively licensed open-source context-bounded model checker to verify Solidity smart contracts. It can automatically check both predefined safety properties (e.g., bounds checks, overflow, underflow) and user-defined program assertions.

To verify the Solidity smart contract, ESBMC should be built with the option:

-DENABLE_SOLIDITY_FRONTEND=On

Preparing the Python frontend (optional)

The Python frontend enables the analysis of Python code, leveraging the AST (Abstract Syntax Tree) generated by ast2json Python package.

To use the Python frontend, follow these steps:

First install ast2json:

pip3 install ast2json

then enable the Python frontend during the ESBMC build:

-DENABLE_PYTHON_FRONTEND=On

Preparing IBEX as the constraint programming solver for interval contraction (optional)

ESBMC can use the forward and backward operations from constraint programming to contract the search space exploration from the program’s entry point to the property being verified and vice versa. This (interval) contraction is enabled via the option –goto-contractor. First, the IBEX library must be installed using the instructions available at http://ibex-team.github.io/ibex-lib/install.html. Once IBEX is installed on your computer, ESBMC should be built with the option:

-DENABLE_GOTO_CONTRACTOR=ON -DIBEX_DIR=path-to-ibex

Setting Up Solvers

ESBMC relies on SMT solvers to reason about formulae in its back-end.

Currently we support the following solvers: Bitwuzla, Boolector, CVC4, MathSAT, Yices 2, and Z3.

Since this guide focuses primarily on the ESBMC build, we will only cover the steps needed for it.

Note that all solvers are optional, and you don’t need to enable them. However, without any solver, ESBMC will not be able to verify many programs. It is recommended to include at least the SMT solver Boolector.

Setting Up Boolector

We have wrapped the entire build and setup of Boolector in the following command:

git clone --depth=1 --branch=3.2.3 https://github.com/boolector/boolector && cd boolector && ./contrib/setup-lingeling.sh && ./contrib/setup-btor2tools.sh && ./configure.sh --prefix $PWD/../boolector-release && cd build && make -j9 && make install && cd .. && cd ..

For more details on Boolector, please refer to its Github.

Setting Up CVC4 (Linux Only)

We have wrapped the entire build and setup of CVC4 in the following command:

pip3 install toml && git clone https://github.com/CVC4/CVC4.git && cd CVC4 && git reset --hard b826fc8ae95fc && ./contrib/get-antlr-3.4 && ./configure.sh --optimized --prefix=../cvc4 --static --no-static-binary && cd build && make -j4 && make install && cd .. && cd ..

If you need more details on CVC4, please refer to its Github.

Setting Up CVC5

We have wrapped the entire build and setup of CVC5 in the following command:

pip3 install toml &&
git clone https://github.com/CVC5/CVC5.git &&
cd CVC5 &&
git switch --detach cvc5-1.1.2 &&
./configure.sh --prefix=../cvc5 --auto-download --static --no-static-binary &&
cd build && make -j4 && make install && cd .. &&
cd ..

If you need more details on CVC5, please refer to its Github.

Setting Up MathSAT

We have wrapped the entire build and setup of MathSAT in the following command:

Linux:
wget http://mathsat.fbk.eu/release/mathsat-5.5.4-linux-x86_64.tar.gz -O mathsat.tar.gz && tar xf mathsat.tar.gz && mv mathsat-5.5.4-linux-x86_64 mathsat

macOS:
wget http://mathsat.fbk.eu/release/mathsat-5.5.4-darwin-libcxx-x86_64.tar.gz -O mathsat.tar.gz && tar xf mathsat.tar.gz && mv mathsat-5.5.4-darwin-libcxx-x86_64 mathsat

In macOS, the following command is required:

ln -s /usr/local/include/gmp.h mathsat/include/gmp.h

For more details on MathSAT, please refer to its webpage.

Setting Up Yices

First, we need to setup and build GMP library, by entering the following command (Linux only):

wget https://gmplib.org/download/gmp/gmp-6.1.2.tar.xz && tar xf gmp-6.1.2.tar.xz && rm gmp-6.1.2.tar.xz && cd gmp-6.1.2 && ./configure --prefix $PWD/../gmp --disable-shared ABI=64 CFLAGS=-fPIC CPPFLAGS=-DPIC && make -j4 && make install && cd ..

Then, we can build and set up Yices 2 using the following command:

Linux:
git clone https://github.com/SRI-CSL/yices2.git && cd yices2 && git checkout Yices-2.6.4 && autoreconf -fi && ./configure --prefix $PWD/../yices --with-static-gmp=$PWD/../gmp/lib/libgmp.a && make -j9 && make static-lib && make install && cp ./build/x86_64-pc-linux-gnu-release/static_lib/libyices.a ../yices/lib && cd ..

macOS:
git clone https://github.com/SRI-CSL/yices2.git && cd yices2 && git checkout Yices-2.6.4 && autoreconf -fi && ./configure --prefix $PWD/../yices && make -j9 && make static-lib && make install && cp ./build/x86_64-apple-darwin*release/static_lib/libyices.a ../yices/lib && cd ..

If you need more details on Yices 2, please refer to its Github.

Setting Up Z3

We have wrapped the entire build and setup of Z3 in the following command:

Linux:
wget https://github.com/Z3Prover/z3/releases/download/z3-4.13.3/z3-4.13.3-x64-glibc-2.35.zip && unzip z3-4.13.3-x64-glibc-2.35.zip && mv z3-4.13.3-x64-glibc-2.35 z3

macOS:
brew install z3

If you need more details on Z3, please refer to its Github.

If you are using macOS and have installed z3 using brew, you’ll need to copy the entire z3 directory from the place where Homebrew keeps packages to your workspace:

cp -rp $(brew info z3 | egrep "/usr[/a-zA-Z\.0-9]+ " -o) z3

Setting Up Bitwuzla

We have wrapped the entire build and setup of Bitwuzla in the following command:

Linux/macOS:
git clone --depth=1 --branch=0.8.2 https://github.com/bitwuzla/bitwuzla.git && cd bitwuzla && ./configure.py --prefix $PWD/../bitwuzla-release && cd build && meson install

For more details on Bitwuzla, please refer to its Github.

Before proceeding to the next section, make sure you have clang, LLVM, and all the solvers ready in your workspace:

clang and LLVM:
<path_to_your_project>/ESBMC_Project/clang13

Boolector:
<path_to_your_project>/ESBMC_Project/boolector

CVC4: (Linux only)
<path_to_your_project>/ESBMC_Project/CVC4

MathSAT:
<path_to_your_project>/ESBMC_Project/mathsat

Yices:
<path_to_your_project>/ESBMC_Project/yices

Z3:
<path_to_your_project>/ESBMC_Project/z3

Bitwuzla:
<path_to_your_project>/ESBMC_Project/bitwuzla

The above paths will be used in ESBMC’s build command in the next section.

If you are using macOS, make sure you have Xcode.app in your Applications directory by checking:

ls /Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk/usr/include/

If no such directory, please go to App Store and install Xcode. If you do not have the full version of Xcode, you will need to replace the flag C2GOTO with:

-DC2GOTO_SYSROOT=/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk

Building ESBMC

Now we are ready to build ESBMC. Please note that we describe the same build option used in our CI/CD. If you want to all available cmake options, refer to our Options.cmake file.

If you are building ESBMC-CHERI, please complete the following sections BEFORE configuring ESBMC-CHERI:

• Preparing CHERI Clang 13 (experimental)
  • This section helps you to build CHERI-LLVM and set up ESBMC_CLANG.
• Setting up the sysroot for CHERI clang
  • This section will get you the CHERI header files to set up ESBMC_CHERI_HYBRID_SYSROOT and ESBMC_CHERI_PURECAP_SYSROOT.

First, we need to setup cmake, by using the following command in ESBMC_Project directory you just created:

Linux:
cd esbmc && mkdir build && cd build && cmake .. -GNinja -DBUILD_TESTING=On -DENABLE_REGRESSION=On $ESBMC_CLANG -DBUILD_STATIC=${ESBMC_STATIC:-ON} -DBoolector_DIR=$PWD/../../boolector-release -DZ3_DIR=$PWD/../../z3 -DENABLE_MATHSAT=ON -DMathsat_DIR=$PWD/../../mathsat -DENABLE_YICES=On -DYices_DIR=$PWD/../../yices -DCVC4_DIR=$PWD/../../cvc4 -DGMP_DIR=$PWD/../../gmp -DBitwuzla_DIR=$PWD/../../bitwuzla-release -DCMAKE_INSTALL_PREFIX:PATH=$PWD/../../release

macOS:
cd esbmc && mkdir build && cd build && cmake .. -GNinja -DBUILD_TESTING=On -DENABLE_REGRESSION=On -DBUILD_STATIC=${ESBMC_STATIC:-ON} $ESBMC_CLANG -DLLVM_DIR=/opt/homebrew/opt/llvm@21/lib/cmake/llvm -DClang_DIR=/opt/homebrew/opt/llvm@21/lib/cmake/clang -DBoolector_DIR=$PWD/../../boolector-release -DZ3_DIR=$PWD/../../z3 -DENABLE_MATHSAT=On -DMathsat_DIR=$PWD/../../mathsat -DENABLE_YICES=ON -DYices_DIR=$PWD/../../yices -DC2GOTO_SYSROOT=/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX.sdk -DBitwuzla_DIR=$PWD/../../bitwuzla-release -DCMAKE_INSTALL_PREFIX:PATH=$PWD/../../release

macOS-specific notes:

• LLVM version: Install LLVM 21 via Homebrew: brew install llvm@21. Do not use DOWNLOAD_DEPENDENCIES=ON as it downloads Linux versions incompatible with macOS.

Note, this command uses the ESBMC_CLANG and ESBMC_STATIC variables set in the section on preparing Clang. Note also that if you want to enable the debug mode, i.e., the internal assertions in ESBMC, you must add the option -DCMAKE_BUILD_TYPE=Debug.

Finally, we can trigger the build process by using the following command:

cmake --build . && ninja install

Once it is finished, ESBMC should be available in the release folder.

ESBMC Shared Builds

It is also possible to build a non-static version of ESBMC that links to system libraries and/or solvers installed system-wide.

Shared linking is the default when cmake is invoked with -DBUILD_STATIC=Off or the variable is not set.

Notes on shared Clang

When clang has been built with the cmake setting CLANG_LINK_CLANG_DYLIB=On, the default is to link against the dynamic library libclang-cpp and also to not bundle clang’s header files. This bundling can be controlled by setting the cmake variable CLANG_HEADERS_BUNDLED to On or Off instead of its default detect.

On means that the headers are always bundled in ESBMC’s executables, and Off never bundles the headers, but hard-codes their path. Not bundling headers when linking shared against a system installation of clang speeds up ESBMC’s translation of source files by avoiding the creation of a temporary directory and extracting the bundled headers to it. As is common with runtime dependencies on shared libraries, when clang is updated to a new version, ESBMC will need to be recompiled.

It is advised to keep the default setting detect for CLANG_HEADERS_BUNDLED, which decides to bundle headers only when linking statically against clang.

Setting up the sysroot for CHERI clang

CHERI clang is used as frontend by CHERI-enabled ESBMC. Since CHERI support is available only for a few platforms, verifying CHERI-C programs that use header files from the C standard library will require a setup of a C standard library for one of these platforms.

To obtain and install a CHERI sysroot, the cheribuild tool is the recommended way:

The following command will install the packages required for the most commonly used cheribuild targets:

sudo apt install autoconf automake libtool pkg-config clang bison cmake mercurial ninja-build samba flex texinfo time libglib2.0-dev libpixman-1-dev libarchive-dev libarchive-tools libbz2-dev libattr1-dev libcap-ng-dev libexpat1-dev libgmp-dev bc

Download and build Cheri riscv64 purecap sdk:

git clone https://github.com/CTSRD-CHERI/cheribuild.git && cd cheribuild && python3 cheribuild.py cheribsd-sdk-riscv64-purecap -d

Once the build is completed, you’ll find the cheri directory in your HOME directory.

CHERI-enabled ESBMC defaults to the platform mips64-unknown-freebsd and expects the corresponding sysroot, the default of which can be configured by passing the CMake flags

-DESBMC_CHERI=On -DESBMC_CHERI_HYBRID_SYSROOT=<path> -DESBMC_CHERI_PURECAP_SYSROOT=<path>

e.g. the ‘path’ should point to $HOME/cheri/output/sdk/sysroot-riscv64-purecap. As for the sysroot-riscv64-purecap part, you may want to use a diffrent directory if you used a different variant in the cheribuild.py command above.

ESBMC Fuzzing Tests

ESBMC has a number of fuzzing test targets that are used with libFuzzer to test parts of ESBMC. Building these targets requires additional CMake configuration.

Using Clang to build the fuzzing targets is required due to the included libFuzzer support. Clang must therefore be installed and CMake configured to use Clang to build ESBMC. One way to do this is to pass the following options to CMake:

-DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++

Note that passing these options to CMake for the first time will result in the CMake cache being deleted, possibly requiring some variables to be reset.

Fuzzing tests must also be enabled with -DENABLE_FUZZER=1 before building.