Proof include fixes

Skptak · Aug 20, 2023 · e98ca67 · e98ca67
1 parent 7b155b1
commit e98ca67
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 7 deletions.
diff --git a/test/cbmc/include/get_time_stub.h b/test/cbmc/include/get_time_stub.h
@@ -31,6 +31,8 @@
 #ifndef GET_TIME_STUB_H_
 #define GET_TIME_STUB_H_
 
+#include <stdint.h>
+
 /**
  * Application defined callback to retrieve the current time in milliseconds.
  *

diff --git a/test/cbmc/proofs/HTTPClient_Send/HTTPClient_Send_harness.c b/test/cbmc/proofs/HTTPClient_Send/HTTPClient_Send_harness.c
@@ -28,8 +28,8 @@
  * @brief Implements the proof harness for HTTPClient_Send function.
  */
 
-#include "core_http_client.h"
 #include "get_time_stub.h"
+#include "core_http_client.h"
 #include "http_cbmc_state.h"
 #include "transport_interface_stubs.h"
 
@@ -61,11 +61,10 @@ void HTTPClient_Send_harness()
     {
         /* Ideally, we want to set the function pointers below with
          * __CPROVER_assume() but doing so makes CBMC run out of memory. */
-        pTransportInterface->send = nondet_bool() ? NULL
-                                                  : TransportInterfaceSendStub;
-        pTransportInterface->recv = nondet_bool()
-                                        ? NULL
-                                        : TransportInterfaceReceiveStub;
+        /* clang-format off */
+        pTransportInterface->send = nondet_bool() ? NULL : TransportInterfaceSendStub;
+        pTransportInterface->recv = nondet_bool() ? NULL : TransportInterfaceReceiveStub;
+        /* clang-format on */
     }
 
     if( pResponse != NULL )

diff --git a/test/cbmc/stubs/get_time_stub.c b/test/cbmc/stubs/get_time_stub.c
@@ -27,9 +27,11 @@
  * @file get_time_stub.c
  * @brief A stub to mock the retrieval of current time.
  */
-#include "get_time_stub.h"
+/* LibC Includes */
 #include "stdint.h"
 
+#include "get_time_stub.h"
+
 uint32_t GetCurrentTimeStub( void )
 {
     /* The HTTP relies on this timestamp in order to complete the network send