Skip to content

CBMC starter kit setup script

Jump to bottom
Mark R. Tuttle edited this page Oct 28, 2020 · 1 revision

The script scripts/setup.py will install a collection of templates for building and checking CBMC proofs. Set environment variable as described in the list of starter kit directories. Then run the script. It will ask you for

  • the source root (which is ${SRCDIR}) and for
  • the path to the litani executable (which is ${CBMC_ROOT}/litani/litani).

For example,

cd ${CBMC_ROOT}
python3 aws-templates-for-cbmc-proofs/scripts/setup.py
  What is the path to the source root? /usr/project
  What is the path to the litani script? ./litani/litani

The script will install four directories:

  • include: Extra include files for your proofs go here.
  • sources: Extra source code for your proofs goes here. For example, you might write a method allocate_header to allocate a header struct taken as input by several of the functions you are proving correct.
  • stubs: Stubs for your proofs go here. For example, you might write stubs read and write for the methods used to read and write a device controlled by several of the functions you are proving correct.
  • proofs: This is the subtree containing your proofs. This is the root of the proof subtree denoted by PROOF_ROOT in the instructions above.

The script will install three Makefiles:

The script copies some files into place (like Makefile-project-defines and Makefile-project-targets) and creates symbolic links into the starter kit submodule for others (like Makefile.common).

It is not common, but you can rerun the script at any time. One reason to do this is because a file has been added to the starter kit and you want to copy it into place. The script will never overwrite an existing file. This means that important files like Makefile-project-defines will never be overwritten by an empty template just by rerunning the script. If you want to replace an existing file, you must delete the file before running the script.

It is common to update the starter kit submodule. One reason to do this is to get the latest verison of Makefile.common. Because the script installs a symbolic link to Makefile.common in the starter kit submodule, it is enough to advance the starter kit submodule to get the latest version of the file.

Clone this wiki locally