Skip to content

Install CBMC starter kit

Jump to bottom
Mark Tuttle edited this page Oct 23, 2020 · 4 revisions

This repository includes templates and scripts intended to make it easy to get started writing CBMC proofs for your code. The first script installs proof infrastructure in the form of a few directories containing code, templates, and Makefiles that facilitate writing CBMC proofs in general. The second script installs, for a particular proof, a directory containing skeletons of all the files needed to start writing that proof.

Proof infrastructure set up

The script scripts/setup.py will set up the infrastructure for CBMC proofs.

  • Choose the path to the source root (eg, /usr/project)
  • Choose the path to a directory under the source root that should hold the infrastructure (eg, /usr/project/cbmc)
  • Submodule the AWS-templates-for-CBMC repository into this directory (eg, /usr/project/cbmc/aws-templates-for-cbmc) 
    cd /usr/project/cbmc
git submodule add https://github.com/awslabs/aws-templates-for-cbmc-proofs.git aws-templates-for-cbmc-proofs
  • Use the script aws-templates-for-cbmc-proofs/scripts/setup.py to setup the standard directory structure for CBMC proof. 
    cd /usr/project/cbmc
python3 aws-templates-for-cbmc-proofs/scripts/setup.py
    The script will ask for the path to the source root /usr/project. The script will install the directories
    • include: contains include files for the proofs
    • sources: contains source code for the proofs
    • stubs: contains stubs for the proofs
    • proofs: contains the proofs themselves (the proof root).

Proof set up

The script scripts/setup-proof.py will set up a directory for a CBMC proof.

  • Change to a directory under the proof root (/usr/project/cbmc/proofs)
  • Run the script aws-templates-for-cbmc/scripts/setup-proof.py and give
    • The name of the function under test.
    • The path to the source file defining the function under test.
    • The path to the source root

The script will create a directory named for the function, and will install files needed to run the proof.

You can cut and paste into the files, and type make to run and debug the proof.

Clone this wiki locally