28 lines
983 B
Markdown
28 lines
983 B
Markdown
CBMC proofs
|
|
===========
|
|
|
|
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.
|