Skip to content

Installation

Jump to bottom
Jim Grundy edited this page Aug 2, 2021 · 17 revisions

Primary Tools

The primary tools needed are as follows, though several prerequisites need to be installed first:

  • CBMC: The C Bounded Model Checker
  • CBMC Viewer: A report generator for CBMC proofs

Prerequisites

To install and run CBMC and the Viewer you need several prerequisites; you likely have some of these installed already:

  • Python3: A scripting language
  • Exuberant Ctags: A source code indexing facility (required for the CBMC Viewer)
  • Ninja: A performant build system
  • GnuPlot: A graph generating tool for reports
  • GraphViz: Another graph generating tool for reports
  • Jinja2: A template library for Python
  • Voluptuous: A Python validation library

Prerequisite Installation

MacOS

  • If “brew” is not already in your path then install HomeBrew following the instructions on the HomeBrew home page (https://brew.sh/)

  • If “python3” is not already in your path then use HomeBrew to instal it as follows:

    brew install python3

  • Use HomeBrew to install any of the non-Python prerequisites you may be missing

    brew install ctags ninja gnuplot graphviz

  • Use the Python pip installer to install any of the Python prerequisites may be missing

    sudo python3 -m pip install jinja2 voluptuous

Ubuntu

  • Use apt-get to to install any of the non-Python prerequisites you may be missing

    sudo apt-get install ctags ninja-build gnuplot graphviz

  • Use the Python pip installer to install any of the Python prerequisites may be missing

    sudo python3 -m pip install jinja2 voluptuous

Windows

Install Primary Tools

Clone this wiki locally