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": ["/"],

test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/Makefile.json

@@ -2,6 +2,9 @@
   "ENTRY": "vProcessGeneratedUDPPacket",
   "CBMCFLAGS":
   [
+    "--unwind 1",
+    "--unwindset FreeRTOS_InterfaceEndPointOnNetMask.0:3",
+    "--nondet-static"
   ],
   "OBJS":
   [

test/cbmc/proofs/run-cbmc-proofs.py

@@ -186,7 +186,7 @@ def add_proof_jobs(proof_directory, proof_root):
 
     # Run 3 CBMC tasks
 
-    cbmc_out = str(proof_directory / "cbmc.txt")
+    cbmc_out = str(proof_directory / "cbmc.xml")
     run_cmd([
         "litani", "add-job",
         "--command", "make cbmc",
@@ -301,12 +301,12 @@ def main():
     if not args.no_standalone:
         run_build(args.parallel_jobs)
 
-    out_sym = pathlib.Path("/tmp")/"litani"/"runs"/"latest"
-    out_dir = out_sym.resolve()
+        out_sym = pathlib.Path("/tmp")/"litani"/"runs"/"latest"
+        out_dir = out_sym.resolve()
 
-    local_copy = pathlib.Path("output")/"latest"
-    local_copy.parent.mkdir(exist_ok=True)
-    local_copy.symlink_to(out_dir)
+        local_copy = pathlib.Path("output")/"latest"
+        local_copy.parent.mkdir(exist_ok=True)
+        local_copy.symlink_to(out_dir)
 
 
 if __name__ == "__main__":