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.
