CBMC starter kit installation

Installation

Installing the starter kit involves three steps. Set the variable CBMC_ROOT to the root of the CBMC subtree as described in the list of starter kit directories.

• Install the starter kit itself.

  cd ${CBMC_ROOT}
  git submodule add https://github.com/awslabs/aws-templates-for-cbmc-proofs.git aws-templates-for-cbmc-proofs
  

• Install litani, a build tool used by the starter kit that makes it easy to build and check proofs concurrently.

  cd ${CBMC_ROOT}
  git submodule add https://github.com/awslabs/aws-build-accumulator.git litani
  

• Install ninja (a build tool used by litani) and gnuplot (a graphical tool used by litani) and the python packages jinja and voluptuous:

  On MacOS:   
    brew install ninja gnuplot
    sudo python3 -m pip install jinja2 voluptuous
  
  On Ubuntu:  
    sudo apt-get install ninja-build gnuplot
    sudo python3 -m pip install jinja2 voluptuous
  
  On Windows: 
    ninja: Download from https://github.com/ninja-build/ninja/releases
    gnuplot: Download from http://www.gnuplot.info/download.html
    python3 -m pip install jinja2 voluptuous
  

Set up

Setting up the starter kit involves two steps:

• Run the setup script to install templates to build and check CBMC proofs.
• Run the proof setup script once for each proof to install templates to build and check a specific CBMC proof.

Litani

You can learn more about the build tool litani used by the starter kit from the litani manual.