README.md
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