-
Notifications
You must be signed in to change notification settings - Fork 21
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 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. We require Python 3.7 or later.
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
Install the tool dependencies with
sudo apt-get install python3 python3-pip ctags ninja-build gnuplot graphviz
sudo python3 -m pip install jinja2 voluptuous
Install the binary tool dependencies by downloading them from
- python: Download from https://www.python.org/downloads/windows/
- 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 themselves from the tool release pages:
- CBMC: Follow the instructions on the CBMC release page.
- CBMC viewer: Follow the instructions on the CBMC viewer release page.
The dependencies mentioned on these release pages have already been installed by the dependency installation instructions given above.
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