Installation

The starter kit is a command line tool distributed as both a brew package and a pip package. The starter kit release page gives installation instructions that we repeat here.

Note: The starter kit used to be distributed as a git repository that you submoduled into your own repository. The starter kit is now distributed as a command line tool. Follow the update instructions below to upgrade your project from using the submodule to using the command line tool.

Installing with brew

On MacOS, we recommend using brew to install the starter kit:

brew tap aws/tap
brew install cbmc-starter-kit cbmc-viewer litani

The brew home page gives instructions for installing brew. The command brew tap aws/tap taps the AWS repository that contains the brew packages. The cbmc-viewer and litani packages are tools used by the starter kit. See the cbmc-viewer release page and the litani release page for other ways to install them if you don't want to use brew.

Installing with pip

On any machine, you can use pip to install the starter kit:

python3 -m pip install cbmc-starter-kit cbmc-viewer

The python download page gives instructions for installing python and pip. The cbmc-viewer and litani packages are tools used by the starter kit. See the cbmc-viewer release page and the litani release page for installation instructions (we used pip to install cbmc-viewer in the command above).

Installing for developers

Developers can install the package in "editable mode" which makes it possible to modify the code in the source tree and then run the command from the command line as usual to test the changes. First, install cbmc-viewer and litani as described above if you haven't already. Then

Clone the repository and install dependencies with

git clone https://github.com/model-checking/cbmc-starter-kit cbmc-starter-kit
python3 -m pip install virtualenv gitpython

Install into a virtual environment with
```
cd cbmc-starter-kit
make develop
```
At this point you can either activate the virtual environment with
```
source /tmp/cbmc-starter-kit/bin/activate
```
or simply add the virtual environment to your path with
```
export PATH=/tmp/cbmc-starter-kit/bin:$PATH
```
Uninstall with
```
cd cbmc-starter-kit
make undevelop
```

Updating

To update to the the latest version of the starter kit:

Update the starter kit itself with

brew upgrade cbmc-starter-kit

python3 -m pip install cbmc-starter-kit --upgrade

Update your repository by changing to the cbmc directory that contains the proofs directory installed by the starter kit and running the update script:
```
cd cbmc
cbmc-starter-kit-update
```
This will overwrite Makefile.common and run-cbmc-proofs.py in the proofs directory with the latest versions.

Updating to the command line tool

The starter kit used to be distributed as a git repository that you submoduled into your own repository. The same used to be true for litani, the build tool used by the starter kit. Now both are distributed a command line tools. We recommend that you migrate to using these command line tools.

Install the starter kit and litani as command line tools
- On MacOS
```
brew install cbmc-starter-kit litani
```
- On Ubuntu, first download the litani debian package from the litani release page then
```
python3 -m pip install cbmc-starter-kit
apt install ./litani-*.deb
```
Change to the cbmc directory that contains the proofs directory installed by the starter kit, and run the update script
```
cd cbmc
cbmc-starter-kit-update --remove-starter-kit-submodule --remove-litani-submodule
```
This will overwrite Makefile.common and run-cbmc-proofs.py in the proofs directory with the latest versions, and remove the submodules for the starter kit and litani if they are present. It will also perform some cleanup actions, such as replacing symbolic links into the starter kit submodule with copies of the files being linked to, and removing a set of negative tests that are rarely used.

See cbmc-starter-kit-update for more information.

While you are at it, we have changed the starter kit license from Apache 2.0 to MIT-0, and you might want to run a script to change copyright headers from Apache to MIT in files under the cbmc directory:

cd cbmc
cbmc-starter-kit-migrate-license --remove

See cbmc-starter-kit-migrate-license for more information.

Installation notes

If you have difficulty installing these tools, please let us know by submitting a GitHub issue.

CBMC starter kit