Generate correct cbmc-batch.yaml locally (#1988)

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Author: feliperodri

tests/cbmc/proofs/Makefile.cbmc_batch

@@ -50,7 +50,7 @@ define yaml_encode_options
        "$(shell echo $(1) | sed 's/ ,/ /g' | sed 's/ /;/g')"
 endef
 
-$(ENTRY).yaml: 
+$(ENTRY).yaml:
 	echo 'batchpkg: $(BATCHPKG)' > $@
 	echo 'build: true' >> $@
 	echo 'cbmcflags: $(call yaml_encode_options,$(CHECKFLAGS) $(CBMCFLAGS))' >> $@
@@ -64,12 +64,18 @@ $(ENTRY).yaml:
 
 batch-yaml: $(ENTRY).yaml Makefile
 
-cbmc-batch.yaml: 
+cbmc-batch.yaml:
 	echo 'cbmcflags: $(strip $(call yaml_encode_options,$(CHECKFLAGS) $(CBMCFLAGS)))' > $@
 	echo 'expected: "SUCCESSFUL"' >> $@
 	echo 'goto: gotos/$(ENTRY).goto' >> $@
 	echo 'jobos: ubuntu16' >> $@
 
+empty-cbmc-batch.yaml:
+	echo ':' > 'cbmc-batch.yaml'
+	echo '  This file marks this directory as containing a CBMC proof. This file' >> 'cbmc-batch.yaml'
+	echo '  is automatically clobbered in CI and replaced with parameters for' >> 'cbmc-batch.yaml'
+	echo '  running the proof.' >> 'cbmc-batch.yaml'
+
 ci-yaml: cbmc-batch.yaml Makefile
 
 .PHONY: ci-yaml batch-yaml

tests/cbmc/proofs/s2n_blob_init/cbmc-batch.yaml

@@ -1,4 +1,4 @@
-cbmcflags: "--bounds-check;--conversion-check;--div-by-zero-check;--enum-range-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--object-bits;8"
-expected: "SUCCESSFUL"
-goto: gotos/s2n_blob_init_harness.goto
-jobos: ubuntu16
+:
+  This file marks this directory as containing a CBMC proof. This file
+  is automatically clobbered in CI and replaced with parameters for
+  running the proof.

tests/cbmc/proofs/s2n_blob_is_growable/cbmc-batch.yaml

@@ -1,4 +1,4 @@
-cbmcflags: "--bounds-check;--conversion-check;--div-by-zero-check;--enum-range-check;--float-overflow-check;--nan-check;--pointer-check;--pointer-overflow-check;--pointer-primitive-check;--signed-overflow-check;--undefined-shift-check;--unsigned-overflow-check;--unwind;1;--unwinding-assertions;--object-bits;8"
-expected: "SUCCESSFUL"
-goto: gotos/s2n_blob_is_growable_harness.goto
-jobos: ubuntu16
+:
+  This file marks this directory as containing a CBMC proof. This file
+  is automatically clobbered in CI and replaced with parameters for
+  running the proof.