Need to include core_mqtt.h in the proofs

FreeRTOS · Aug 19, 2023 · 8de943b · 8de943b
1 parent 26f7f69
commit 8de943b
Show file tree

Hide file tree

Showing 5 changed files with 13 additions and 2 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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.