Make explicit that stringBuilder CBMC proof is bounded

With CBMC v6, unwinding assertions are enabled by default.
aws · Jun 6, 2024 · f588952 · f588952
1 parent 7a108e8
commit f588952
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/test/cbmc/proofs/stringBuilder/Makefile b/test/cbmc/proofs/stringBuilder/Makefile
@@ -10,9 +10,11 @@ DEFINES +=
 INCLUDES +=
 
 REMOVE_FUNCTION_BODY +=
-UNWINDSET +=
+UNWINDSET += stringBuilder_harness.0:10
+UNWINDSET += stringBuilder_harness.1:10
+UNWINDSET += stringBuilder.0:10
 
-CBMC_FLAG_UNWINDING_ASSERTIONS =
+CBMC_FLAG_UNWINDING_ASSERTIONS = --no-unwinding-assertions
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/source/ota_mqtt.c