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.
FreeRTOS · Sep 25, 2024 · c7f5440 · c7f5440
1 parent efe1b51
commit c7f5440
Show file tree

Hide file tree

Showing 12 changed files with 225 additions and 185 deletions.
diff --git a/.github/workflows/ci.yml b/.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:

diff --git a/test/cbmc/proofs/MQTTAgentCommand_Connect/Makefile b/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
diff --git a/test/cbmc/proofs/MQTTAgentCommand_Disconnect/Makefile b/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
diff --git a/test/cbmc/proofs/MQTTAgentCommand_Ping/Makefile b/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
diff --git a/test/cbmc/proofs/MQTTAgentCommand_Publish/Makefile b/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
diff --git a/test/cbmc/proofs/MQTTAgentCommand_Subscribe/Makefile b/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
diff --git a/test/cbmc/proofs/MQTTAgentCommand_Unsubscribe/Makefile b/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
diff --git a/test/cbmc/proofs/MQTTAgent_CancelAll/Makefile b/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
diff --git a/test/cbmc/proofs/MQTTAgent_CommandLoop/Makefile b/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
diff --git a/test/cbmc/proofs/MQTTAgent_Init/Makefile b/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
diff --git a/test/cbmc/proofs/MQTTAgent_ResumeSession/Makefile b/test/cbmc/proofs/MQTTAgent_ResumeSession/Makefile
@@ -46,5 +46,6 @@ 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