1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
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.
|
