Skip to content

CBMC starter kit makefile common

Mark R. Tuttle edited this page Oct 28, 2020 · 1 revision

The file Makefile.common is a makefile that defines best practices for building and checking CBMC proofs.

Do not edit this file.

Almost always you will build and check your proof using simply make report. But this makefile does define four targets that you will find helpful:

  • make goto: Compile your code and build the goto binary used by CBMC.
  • make result: Do property checking (eg, check for buffer overflow with CBMC).
  • make coverage: Do coverage checking (eg, compute the lines of code exercised by CBMC).
  • make report: Generate a report summarizing the results of CBMC with CBMC viewer.