diff --git a/test/cbmc/proofs/OtaReceiveEvent_FreeRTOS/OtaReceiveEvent_FreeRTOS_harness.c b/test/cbmc/proofs/OtaReceiveEvent_FreeRTOS/OtaReceiveEvent_FreeRTOS_harness.c index 7b4e5dcbd..fee5d0b41 100644 --- 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 + +/* 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 index d073c501a..ddc0c6ea6 100644 --- 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 + +/* 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 ) {