Installation

This page gives instructions for installing the verification tools

• CBMC: The C Bounded Model Checker
• CBMC Viewer: A CBMC proof viewer

and their dependencies

• Python3: A scripting language
• Exuberant Ctags: A source code indexing facility
• Ninja: A performant build system
• GnuPlot: A graph generating tool for reports
• GraphViz: Another graph generating tool for reports
• Jinja2: A Python template package
• Voluptuous: A Python validation package

Install the tool dependencies

Install the tool dependencies by cutting-and-pasting the following commands into your shell. If you have already installed one of these dependencies --- for example, if you have already installed python3 and want to continue using that installation --- you may omit this dependency from the installation commands below.

MacOS

HomeBrew (or simply brew) is a popular package manager for MacOS. Install brew with

  /bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"

Install the tool dependencies with

  brew install python3 ctags ninja gnuplot graphviz
  sudo python3 -m pip install jinja2 voluptuous

Ubuntu

Install the tool dependencies with

  sudo apt-get install python3 python3-pip ctags ninja-build gnuplot graphviz
  sudo python3 -m pip install jinja2 voluptuous

Windows

Install the binary tool dependencies by downloading them from

• ctags: Download from https://sourceforge.net/projects/ctags
• ninja: Download from https://github.com/ninja-build/ninja/releases
• gnuplot: Download from http://www.gnuplot.info/download.html
• graphviz: Download from https://graphviz.org/download/

Install the python dependencies with

  python3 -m pip install jinja2 voluptuous

Install the tools

Install the tools themselves by following the installation instructions on the tool release pages below. The tool dependencies mentioned on these pages have already been installed by the instructions above.

• CBMC: Follow the instructions on the CBMC release page.
• CBMC viewer: Follow the instructions on the CBMC viewer release page.

Test the tools

Test that tools are installed correctly by cutting-and-pasting the following commands into your shell. These commands run the memory safety proof for one method in the FreeRTOS HTTP implementation. Expect this proof to take about a minute to run.

  git clone https://github.com/FreeRTOS/coreHTTP.git
  cd coreHTTP
  git submodule update --init --checkout --recursive

  cd test/cbmc/proofs/HTTPClient_ReadHeader
  make report
  open html/html/index.html

You can run all 20+ memory saftey proofs with the following commands. Expect these commands to take between 6 and 30 minutes to run depending on your machine.

  git clone https://github.com/FreeRTOS/coreHTTP.git
  cd coreHTTP
  git submodule update --init --checkout --recursive

  cd test/cbmc/proofs
  ./run-cbmc-proofs.py
  open /tmp/litani/runs/*/html/index.html