Fix CBMC proof of ProcessDHCPReplies (FreeRTOS#177)

* Update Proof

* Uncrustify and fix one broken proof due to removal of _static

* Uncrustify

* Update the comments

Author: AniruddhaKanhere

FreeRTOS_DHCP.c

@@ -217,8 +217,8 @@
 /*
  * Interpret message received on the DHCP socket.
  */
-    _static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
-                                              NetworkEndPoint_t * pxEndPoint );
+    static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
+                                             NetworkEndPoint_t * pxEndPoint );
 
 /*
  * Generate a DHCP request packet, and send it on the DHCP socket.
@@ -966,8 +966,8 @@
  *
  * @return pdPASS: if DHCP options are received correctly; pdFAIL: Otherwise.
  */
-    _static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
-                                              NetworkEndPoint_t * pxEndPoint )
+    static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
+                                             NetworkEndPoint_t * pxEndPoint )
     {
         uint8_t * pucUDPPayload;
         int32_t lBytes;

test/cbmc/proofs/DHCP/DHCPProcessEndPoint/DHCPProcessEndPoint_harness.c

@@ -97,8 +97,8 @@ Socket_t FreeRTOS_socket( BaseType_t xDomain,
 * Function Abstraction:
 * prvProcessDHCPReplies has been proved memory safe in ProcessDHCPReplies.
 ****************************************************************/
-BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
-                                  NetworkEndPoint_t * pxEndPoint )
+BaseType_t __CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
+                                                                       NetworkEndPoint_t * pxEndPoint )
 {
     return nondet_BaseType();
 }

test/cbmc/proofs/ProcessDHCPReplies/Makefile.json

@@ -26,7 +26,7 @@
   "CBMCFLAGS": [
       # "--nondet-static",
       "--unwind 1",
-      "--unwindset memcmp.0:7,prvProcessDHCPReplies.0:{BUFFER_PAYLOAD}"
+      "--unwindset memcmp.0:7,__CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies.0:{BUFFER_PAYLOAD}"
   ],
 
   "OBJS":
@@ -44,5 +44,11 @@
   [
     "CBMC_DHCPMESSAGE_HEADER_SIZE={BUFFER_HEADER}",
     "CBMC_FREERTOS_RECVFROM_BUFFER_BOUND={BUFFER_SIZE}"
+  ],
+
+  "OPT":
+  [
+    # Flag to access the static function of a file
+    "--export-file-local-symbols"
   ]
 }

test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c

@@ -13,25 +13,34 @@
 #include "FreeRTOS_UDP_IP.h"
 #include "FreeRTOS_DHCP.h"
 #include "FreeRTOS_ARP.h"
-
+#include "FreeRTOS_Routing.h"
 
 /****************************************************************
 * Signature of function under test
+* The function name (prvProcessDHCPReplies) is mangled due to the
+* use of a CBMC flag (--export-file-local-symbols) which allows us
+* to access this static function outside the source file in which
+* it is defined.
 ****************************************************************/
-
-BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType );
+BaseType_t __CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
+                                                                       NetworkEndPoint_t * pxEndPoint );
 
 /****************************************************************
 * The proof for FreeRTOS_gethostbyname.
 ****************************************************************/
-
 void harness()
 {
     /* Omitting model of an unconstrained xDHCPData because xDHCPData is */
     /* the source of uninitialized data only on line 647 to set a */
     /* transaction id is an outgoing message */
 
     BaseType_t xExpectedMessageType;
+    NetworkEndPoint_t xEndPoint;
+
+    /* The function under test is a private (static) function called only by
+     * the TCP stack. The stack asserts that the endpoint cannot be NULL
+     * before the function under test is invoked. */
+    NetworkEndPoint_t * pxEndPoint = &xEndPoint;
 
-    prvProcessDHCPReplies( xExpectedMessageType );
+    __CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies( xExpectedMessageType, pxEndPoint );
 }