From 6799e41ee49ebfdbfa3cc93636d1d5d5de4ab86a Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 23 Aug 2024 13:33:13 +0000
Subject: [PATCH] Adjust proof tooling to support CBMC v6

With CBMC v6, unwinding assertions as well as other checks are enabled
by default.
---
 .github/workflows/ci.yml             | 2 +-
 test/cbmc/proofs/Makefile.template   | 6 +++---
 test/cbmc/proofs/MakefileCommon.json | 4 +---
 3 files changed, 5 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index ba6a8c166..06e55afcd 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -406,7 +406,7 @@ jobs:
       - name: Set up CBMC runner
         uses: FreeRTOS/CI-CD-Github-Actions/set_up_cbmc_runner@main
         with:
-          cbmc_version: "5.95.1"
+          cbmc_version: "6.1.1"
 
       - env:
           stepName: Install Dependencies
diff --git a/test/cbmc/proofs/Makefile.template b/test/cbmc/proofs/Makefile.template
index 15cf815db..847b0a8f2 100644
--- a/test/cbmc/proofs/Makefile.template
+++ b/test/cbmc/proofs/Makefile.template
@@ -124,13 +124,13 @@ goto:
 # report if the proof failed. If the proof failed, we separately fail
 # the entire job using the check-cbmc-result rule.
 cbmc.xml: $(ENTRY).goto
-	-cbmc $(CBMCFLAGS) $(SOLVER) --unwinding-assertions --trace --xml-ui @RULE_INPUT@ > $@ 2>&1
+	-cbmc $(CBMCFLAGS) $(SOLVER) --trace --xml-ui @RULE_INPUT@ > $@ 2>&1
 
 property.xml: $(ENTRY).goto
-	cbmc $(CBMCFLAGS) --unwinding-assertions --show-properties --xml-ui @RULE_INPUT@ > $@ 2>&1
+	cbmc $(CBMCFLAGS) --show-properties --xml-ui @RULE_INPUT@ > $@ 2>&1
 
 coverage.xml: $(ENTRY).goto
-	cbmc $(CBMCFLAGS) --cover location --xml-ui @RULE_INPUT@ > $@ 2>&1
+	cbmc $(CBMCFLAGS) --no-standard-checks --malloc-may-fail --malloc-fail-null --cover location --xml-ui @RULE_INPUT@ > $@ 2>&1
 
 cbmc: cbmc.xml
 
diff --git a/test/cbmc/proofs/MakefileCommon.json b/test/cbmc/proofs/MakefileCommon.json
index 7ada3e1dc..79e8b7bfb 100644
--- a/test/cbmc/proofs/MakefileCommon.json
+++ b/test/cbmc/proofs/MakefileCommon.json
@@ -32,9 +32,7 @@
 
     "CBMCFLAGS ": [
 	"--object-bits 8",
-	"--32",
-	"--bounds-check",
-	"--pointer-check"
+	"--32"
     ],
 
     "FORWARD_SLASH": ["/"],