This directory contains the CBMC proofs. Each proof is in its own directory.

This directory includes four Makefiles.

One Makefile describes the basic workflow for building and running proofs:

• Makefile.common:
  • make: builds the goto binary, does the cbmc property checking and coverage checking, and builds the final report.
  • make goto: builds the goto binary
  • make result: does cbmc property checking
  • make coverage: does cbmc coverage checking
  • make report: builds the final report

Three included Makefiles describe project-specific settings and can override definitions in Makefile.common:

• Makefile-project-defines: definitions like compiler flags required to build the goto binaries, and definitions to override definitions in Makefile.common.
• Makefile-project-targets: other make targets needed for the project
• Makefile-project-testing: other definitions and targets needed for unit testing or continuous integration.