From 8de943bfb41160569f7c79d5a59380af4ed3594d Mon Sep 17 00:00:00 2001
From: Soren Ptak <ptaksoren@gmail.com>
Date: Sat, 19 Aug 2023 00:09:17 -0700
Subject: [PATCH] Need to include core_mqtt.h in the proofs

---
 test/cbmc/include/core_mqtt_config.h        | 3 +++
 test/cbmc/include/event_callback_stub.h     | 3 ++-
 test/cbmc/include/get_time_stub.h           | 3 +++
 test/cbmc/include/mqtt_cbmc_state.h         | 3 ++-
 test/cbmc/include/network_interface_stubs.h | 3 +++
 5 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/test/cbmc/include/core_mqtt_config.h b/test/cbmc/include/core_mqtt_config.h
index 4877b34bd..b3a94b966 100644
--- a/test/cbmc/include/core_mqtt_config.h
+++ b/test/cbmc/include/core_mqtt_config.h
@@ -30,6 +30,9 @@
 #ifndef CORE_MQTT_CONFIG_H_
 #define CORE_MQTT_CONFIG_H_
 
+/* core_mqtt.h must precede including this header. */
+#include "core_mqtt.h"
+
 /* Mock a network context for the CBMC proofs. */
 struct NetworkContext
 {
diff --git a/test/cbmc/include/event_callback_stub.h b/test/cbmc/include/event_callback_stub.h
index 552239e8e..04ebece03 100644
--- a/test/cbmc/include/event_callback_stub.h
+++ b/test/cbmc/include/event_callback_stub.h
@@ -31,7 +31,8 @@
 #ifndef EVENT_CALLBACK_STUB_H_
 #define EVENT_CALLBACK_STUB_H_
 
-/* mqtt.h must precede including this header. */
+/* core_mqtt.h must precede including this header. */
+#include "core_mqtt.h"
 
 /**
  * @brief User defined callback for receiving incoming publishes and incoming
diff --git a/test/cbmc/include/get_time_stub.h b/test/cbmc/include/get_time_stub.h
index 42045a278..3806c8f8b 100644
--- a/test/cbmc/include/get_time_stub.h
+++ b/test/cbmc/include/get_time_stub.h
@@ -31,6 +31,9 @@
 #ifndef GET_TIME_STUB_H_
 #define GET_TIME_STUB_H_
 
+/* core_mqtt.h must precede including this header. */
+#include "core_mqtt.h"
+
 /**
  * Application defined callback to retrieve the current time in milliseconds.
  *
diff --git a/test/cbmc/include/mqtt_cbmc_state.h b/test/cbmc/include/mqtt_cbmc_state.h
index 187a57008..32af0a931 100644
--- a/test/cbmc/include/mqtt_cbmc_state.h
+++ b/test/cbmc/include/mqtt_cbmc_state.h
@@ -32,7 +32,8 @@
 
 #include <stdbool.h>
 
-/* mqtt.h must precede including this header. */
+/* core_mqtt.h must precede including this header. */
+#include "core_mqtt.h"
 
 #define IMPLIES( a, b ) ( !( a ) || ( b ) )
 
diff --git a/test/cbmc/include/network_interface_stubs.h b/test/cbmc/include/network_interface_stubs.h
index 2c61933ef..6fddbb140 100644
--- a/test/cbmc/include/network_interface_stubs.h
+++ b/test/cbmc/include/network_interface_stubs.h
@@ -32,6 +32,9 @@
 #define NETWORK_INTERFACE_STUBS_H_
 
 /* transport_interface.h must precede including this header. */
+/* core_mqtt.h must precede including this header. */
+#include "core_mqtt.h"
+#include "transport_interface.h"
 
 /**
  * @brief Application defined network interface receive function.