diff --git a/src/cbmc_starter_kit/template-for-proof/Makefile b/src/cbmc_starter_kit/template-for-proof/Makefile index d08207a1..dffc1073 100644 --- a/src/cbmc_starter_kit/template-for-proof/Makefile +++ b/src/cbmc_starter_kit/template-for-proof/Makefile @@ -18,7 +18,10 @@ PROJECT_SOURCES += $(SRCDIR)/<__PATH_TO_SOURCE_FILE__> # EXPENSIVE variable. With new enough versions of the proof tools, this will # restrict the number of EXPENSIVE CBMC jobs running at once. See the # documentation in Makefile.common under the "Job Pools" heading for details. +# You may also choose to set ENABLE_POOLS right here, or else set it on the +# command-line (see Makefile.common). # EXPENSIVE = true +# ENABLE_POOLS = true # If you require access to a file-local ("static") function or object to conduct # your proof, set the following (and do not include the original source file diff --git a/src/cbmc_starter_kit/template-for-repository/proofs/Makefile.common b/src/cbmc_starter_kit/template-for-repository/proofs/Makefile.common index 0990615c..a4d680d8 100644 --- a/src/cbmc_starter_kit/template-for-repository/proofs/Makefile.common +++ b/src/cbmc_starter_kit/template-for-repository/proofs/Makefile.common @@ -211,10 +211,13 @@ CHECKFLAGS += $(USE_EXTERNAL_SAT_SOLVER) ifeq ($(strip $(ENABLE_POOLS)),) POOL = + INIT_POOLS = else ifeq ($(strip $(EXPENSIVE)),) POOL = + INIT_POOLS = else POOL = --pool expensive + INIT_POOLS = --pools expensive:1 endif # Similar to the pool feature above. If Litani is new enough, enable @@ -915,7 +918,7 @@ litani-path: _goto: $(HARNESS_GOTO).goto goto: @ echo Running 'litani init' - $(LITANI) init --project $(PROJECT_NAME) + $(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME) @ echo Running 'litani add-job' $(MAKE) -B _goto @ echo Running 'litani build' @@ -924,7 +927,7 @@ goto: _result: $(LOGDIR)/result.txt result: @ echo Running 'litani init' - $(LITANI) init --project $(PROJECT_NAME) + $(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME) @ echo Running 'litani add-job' $(MAKE) -B _result @ echo Running 'litani build' @@ -933,7 +936,7 @@ result: _property: $(LOGDIR)/property.xml property: @ echo Running 'litani init' - $(LITANI) init --project $(PROJECT_NAME) + $(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME) @ echo Running 'litani add-job' $(MAKE) -B _property @ echo Running 'litani build' @@ -942,7 +945,7 @@ property: _coverage: $(LOGDIR)/coverage.xml coverage: @ echo Running 'litani init' - $(LITANI) init --project $(PROJECT_NAME) + $(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME) @ echo Running 'litani add-job' $(MAKE) -B _coverage @ echo Running 'litani build' @@ -951,7 +954,7 @@ coverage: _report: $(PROOFDIR)/report report: @ echo Running 'litani init' - $(LITANI) init --project $(PROJECT_NAME) + $(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME) @ echo Running 'litani add-job' $(MAKE) -B _report @ echo Running 'litani build'