CBMC starter kit directories

Three directories play an important role in the CBMC starter kit. We refer to thse directories in this documentation using environment variables. We recommend that you set these environment variables to values that make sense for your project. Then you can just cut-and-paste the commands given in this documentation directly into your command shell.

These are the directories:

• SRCDIR: This is the root of the source tree. It can be anything, but it is typically the root of a GitHub repository.

  export SRCDIR=/usr/project
  

• CBMC_ROOT: This is the root of the subtree containing the CBMC proof infrastructure installed by this starter kit. It can be anything, but it is particularly convenient if it is located somewhere under the source root. For example, it could be a directory next to the directory that contains your unit tests.

  export CBMC_ROOT=${SRCDIR}/cbmc
  

• PROOF_ROOT: This is the root of the subtree containing the CBMC proofs themselves. This must be the proofs subdirectory of CBMC_ROOT.

  export PROOF_ROOT=${CBMC_ROOT}/proofs