Adjust proof tooling to support CBMC v6

With CBMC v6, unwinding assertions as well as other checks are enabled
by default.

Author: tautschnig

.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

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
 

test/cbmc/proofs/MakefileCommon.json

@@ -32,9 +32,7 @@
 
     "CBMCFLAGS ": [
 	"--object-bits 8",
-	"--32",
-	"--bounds-check",
-	"--pointer-check"
+	"--32"
     ],
 
     "FORWARD_SLASH": ["/"],