Fix CBMC

Author: tony-josi-aws

source/FreeRTOS_DHCPv6.c

@@ -432,6 +432,7 @@ void vDHCPv6Process( BaseType_t xReset,
             BaseType_t xRecvFlags = ( BaseType_t ) FREERTOS_ZERO_COPY;
             struct freertos_sockaddr xSourceAddressCurrent;
             socklen_t xSourceAddressCurrentLength = 0;
+            pucUDPPayload = NULL;
 
             /* Get the next UDP message. */
             lBytes = FreeRTOS_recvfrom( EP_DHCPData.xDHCPSocket, &( pucUDPPayload ), 0, xRecvFlags, &xSourceAddressCurrent, &xSourceAddressCurrentLength );
@@ -443,6 +444,11 @@ void vDHCPv6Process( BaseType_t xReset,
                     FreeRTOS_printf( ( "vDHCPProcess: FreeRTOS_recvfrom returns %d\n", ( int ) lBytes ) );
                 }
 
+                if(pucUDPPayload != NULL)
+                {
+                    FreeRTOS_ReleaseUDPPayloadBuffer( pucUDPPayload );
+                }
+
                 break;
             }
 
@@ -452,7 +458,7 @@ void vDHCPv6Process( BaseType_t xReset,
                 ucFirstIter = 0U;
             }
 
-            /* Verify DHCPv6 server address. */*/
+            /* Verify DHCPv6 server address. */
             if((memcmp(&(xSourceAddress.sin_address.xIP_IPv6.ucBytes), \
             &(xSourceAddressCurrent.sin_address.xIP_IPv6.ucBytes), \
             sizeof(xSourceAddressCurrent.sin_address.xIP_IPv6.ucBytes) ) == 0) &&

test/cbmc/proofs/DHCPv6/DHCPv6Process/DHCPv6Process_harness.c

@@ -153,6 +153,17 @@ int32_t FreeRTOS_recvfrom( Socket_t xSocket,
     return retVal;
 }
 
+/* For the purpose of this proof we stub the 
+ * implementation of FreeRTOS_ReleaseUDPPayloadBuffer here, but make sure that
+ * the pvBuffer is not NULL, its not verified here if the pointer is a valid
+ * payload buffer as its proved in other proofs */
+void FreeRTOS_ReleaseUDPPayloadBuffer( void * pvBuffer )
+{
+    __CPROVER_assert( pvBuffer != NULL,
+                      "FreeRTOS precondition: pvBuffer != NULL" );
+
+}
+
 void harness()
 {
     BaseType_t xReset;

test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json

@@ -5,6 +5,7 @@
     "CBMCFLAGS":
     [
       "--unwind {LOOP_UNWIND_COUNT}",
+      "--unwindset memcmp.0:17",
       "--nondet-static --flush"
     ],
     "OPT":