1CBMC proofs
2===========
3
4This directory contains the CBMC proofs.  Each proof is in its own
5directory.
6
7This directory includes four Makefiles.
8
9One Makefile describes the basic workflow for building and running proofs:
10
11* Makefile.common:
12    * make: builds the goto binary, does the cbmc property checking
13	  and coverage checking, and builds the final report.
14	* make goto: builds the goto binary
15	* make result: does cbmc property checking
16	* make coverage: does cbmc coverage checking
17	* make report: builds the final report
18
19Three included Makefiles describe project-specific settings and can override
20definitions in Makefile.common:
21
22* Makefile-project-defines: definitions like compiler flags
23  required to build the goto binaries, and definitions to override
24  definitions in Makefile.common.
25* Makefile-project-targets: other make targets needed for the project
26* Makefile-project-testing: other definitions and targets needed for
27  unit testing or continuous integration.
28