Proof fixes

aws · Aug 20, 2023 · d8a8788 · d8a8788
1 parent 783518c
commit d8a8788
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 3 deletions.
diff --git a/test/cbmc/proofs/OtaReceiveEvent_FreeRTOS/OtaReceiveEvent_FreeRTOS_harness.c b/test/cbmc/proofs/OtaReceiveEvent_FreeRTOS/OtaReceiveEvent_FreeRTOS_harness.c
@@ -27,11 +27,17 @@
  * @file OtaReceiveEvent_FreeRTOS_harness.c
  * @brief Implements the proof harness for OtaReceiveEvent_FreeRTOS function.
  */
-/* FreeRTOS includes for OTA library. */
-#include "FreeRTOSConfig.h"
+
+/* LibC includes */
+#include <stdlib.h>
+
+/* Proof include */
 #include "ota_os_freertos.h"
 #include "ota_private.h"
 
+/* FreeRTOS includes for OTA library. */
+#include "FreeRTOSConfig.h"
+
 void OtaReceiveEvent_FreeRTOS_harness()
 {
  OtaEventContext_t * pEventCtx;

diff --git a/test/cbmc/proofs/OtaStartTimer_FreeRTOS/OtaStartTimer_FreeRTOS_harness.c b/test/cbmc/proofs/OtaStartTimer_FreeRTOS/OtaStartTimer_FreeRTOS_harness.c
@@ -27,9 +27,15 @@
  * @file OtaStartTimer_FreeRTOS_harness.c
  * @brief Implements the proof harness for OtaStartTimer_FreeRTOS function.
  */
+
+/* LibC includes */
+#include <stdlib.h>
+
+/* Proof include */
+#include "ota_os_freertos.h"
+
 /* FreeRTOS includes for OTA library. */
 #include "FreeRTOSConfig.h"
-#include "ota_os_freertos.h"
 
 void otaCallback( OtaTimerId_t otaTimerId )
 {