CBAT Installation

Table of contents:

Docker Installation

The Dockerfile for CBAT can be found in this directory.

To build the image:

  docker build --tag cbat .

To run the container:

  docker run -it cbat bash

Manual Installation

Prerequisites

Before installing, make sure you have the appropriate dependencies installed. First, there is OCaml:

The recommended way to install Ocaml is with OPAM. Instructions on downloading OPAM, and using OPAM to download Ocaml can be found here.

The following dependencies are needed to install Z3:

You can install the latest Z3 Ocaml bindings from the dev repo with:

  opam pin add z3 --dev-repo

If you want to install the most recent stable release of Z3 from OPAM instead, you can run:

  opam install z3

Next, there is the alpha release of BAP:

Instructions on downloading BAP from the testing repository can be found here.

Then, there are the following OCaml packages:

All of these can be installed with:

  opam install core_kernel ounit2 re dune
Optionally, you may install Boolector 3.2.1 from here to use with the --ext-solver-path option. For some queries, Boolector may be more performant than the standard Z3.

Installing CBAT

Then, to build and install the weakest precondition tools, simply run make in this directory:

  make

To uninstall and clean:

  make clean

To run oUnit unit tests:

  make test

To run oUnit integration tests:

  make test.plugin.integration

To run oUnit tests with colored output, before running the above test commands, run

  export OUNIT_CI=true