Use CBMC 6.0.0 (#1128)

**Issue:**
The proofs broke unexpectedly when CBMC 6.0.0 was released, since we were using "latest". We pinned the version back to  5.95.1 in a [recent PR](#1124) to get CI working again.

**Description of changes:**
- Upgrade to CBMC 6.0.0
    - For all tools used in proofs, stop using "latest". Pin the exact version, so we're not caught off-guard by unexpected upgrades again in the future
- Fix proof code to work with CBMC 6

Author: graebm

.github/workflows/proof_ci_resources/config.yaml

@@ -1,7 +1,8 @@
-cadical-tag: latest
-cbmc-version: "5.95.1"
-cbmc-viewer-version: latest
-kissat-tag: latest
-litani-version: latest
+# Use exact versions (instead of "latest") so we're not broken by surprise upgrades.
+cadical-tag: "rel-2.0.0" # tag of latest release: https://github.com/arminbiere/cadical/releases
+cbmc-version: "6.0.0" # semver of latest release: https://github.com/diffblue/cbmc/releases
+cbmc-viewer-version: "3.8" # semver of latest release: https://github.com/model-checking/cbmc-viewer/releases
+kissat-tag: "rel-3.1.1" # tag of latest release: https://github.com/arminbiere/kissat/releases
+litani-version: "1.29.0" # semver of latest release: https://github.com/awslabs/aws-build-accumulator/releases
 proofs-dir: verification/cbmc/proofs
 run-cbmc-proofs-command: ./run-cbmc-proofs.py

verification/cbmc/proofs/Makefile.common

@@ -465,7 +465,6 @@ COMMA :=,
 # Set C compiler defines
 
 CBMCFLAGS += --object-bits $(CBMC_OBJECT_BITS)
-COMPILE_FLAGS += --object-bits $(CBMC_OBJECT_BITS)
 
 DEFINES += -DCBMC=1
 DEFINES += -DCBMC_OBJECT_BITS=$(CBMC_OBJECT_BITS)

verification/cbmc/sources/utils.c

@@ -170,4 +170,7 @@ uint64_t uninterpreted_hasher(const void *a) {
     return __CPROVER_uninterpreted_hasher(a);
 }
 
-bool uninterpreted_predicate_fn(uint8_t value);
+bool __CPROVER_uninterpreted_predicate_uint8_t(uint8_t);
+bool uninterpreted_predicate_fn(uint8_t value) {
+    return __CPROVER_uninterpreted_predicate_uint8_t(value);
+}