Adjust proof tooling to support CBMC v6

With CBMC v6, unwinding assertions are enabled by default, and object
bits no longer need to be set at compile time. Update various build
rules to use the latest template as provided with CBMC starter kit.

Also fixes use of undefined functions by including the required sources
in proof builds.

Author: tautschnig

.github/workflows/ci.yml

@@ -194,7 +194,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.3.1"
       - name: Run CBMC
         uses: FreeRTOS/CI-CD-Github-Actions/run_cbmc@main
         with:

test/cbmc/proofs/MQTTAgentCommand_Connect/Makefile

@@ -18,4 +18,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_agent_cbmc_state.c
 PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_agent_command_functions.c
 
+PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_agent.c
+
 include ../Makefile.common

test/cbmc/proofs/MQTTAgentCommand_Disconnect/Makefile

@@ -16,5 +16,6 @@ UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_agent_command_functions.c
+PROJECT_SOURCES += $(SRCDIR)/source/dependency/coreMQTT/source/core_mqtt.c
 
 include ../Makefile.common

test/cbmc/proofs/MQTTAgentCommand_Ping/Makefile

@@ -16,5 +16,6 @@ UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_agent_command_functions.c
+PROJECT_SOURCES += $(SRCDIR)/source/dependency/coreMQTT/source/core_mqtt.c
 
 include ../Makefile.common

test/cbmc/proofs/MQTTAgentCommand_Publish/Makefile

@@ -16,5 +16,6 @@ UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_agent_command_functions.c
+PROJECT_SOURCES += $(SRCDIR)/source/dependency/coreMQTT/source/core_mqtt.c
 
 include ../Makefile.common

test/cbmc/proofs/MQTTAgentCommand_Subscribe/Makefile

@@ -16,6 +16,8 @@ UNWINDSET +=
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_agent_cbmc_state.c
+PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_agent.c
 PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_agent_command_functions.c
+PROJECT_SOURCES += $(SRCDIR)/source/dependency/coreMQTT/source/core_mqtt.c
 
 include ../Makefile.common

test/cbmc/proofs/MQTTAgentCommand_Unsubscribe/Makefile

@@ -17,5 +17,6 @@ UNWINDSET +=
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROOF_SOURCES += $(SRCDIR)/test/cbmc/sources/mqtt_agent_cbmc_state.c
 PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_agent_command_functions.c
+PROJECT_SOURCES += $(SRCDIR)/source/dependency/coreMQTT/source/core_mqtt.c
 
 include ../Makefile.common

test/cbmc/proofs/MQTTAgent_CancelAll/Makefile

@@ -39,5 +39,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/agent_command_pool_stubs.c
 PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/agent_message_stubs.c
 PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/core_mqtt_stubs.c
 PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_agent.c
+PROJECT_SOURCES += $(SRCDIR)/source/dependency/coreMQTT/source/core_mqtt.c
 
 include ../Makefile.common

test/cbmc/proofs/MQTTAgent_CommandLoop/Makefile

@@ -53,5 +53,6 @@ PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/agent_command_functions_stub.c
 PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/core_mqtt_stubs.c
 
 PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_agent.c
+PROJECT_SOURCES += $(SRCDIR)/source/dependency/coreMQTT/source/core_mqtt.c
 
 include ../Makefile.common

test/cbmc/proofs/MQTTAgent_Init/Makefile

@@ -17,5 +17,6 @@ UNWINDSET +=
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 
 PROJECT_SOURCES += $(SRCDIR)/source/core_mqtt_agent.c
+PROJECT_SOURCES += $(SRCDIR)/source/dependency/coreMQTT/source/core_mqtt.c
 
 include ../Makefile.common