Fix CBMC proofs for UDP

source/FreeRTOS_UDP_IPv4.c

@@ -297,7 +297,10 @@ void vProcessGeneratedUDPPacket_IPv4( NetworkBufferDescriptor_t * const pxNetwor
                 }
             #endif /* if( ipconfigETHERNET_MINIMUM_PACKET_BYTES > 0 ) */
             iptraceNETWORK_INTERFACE_OUTPUT( pxNetworkBuffer->xDataLength, pxNetworkBuffer->pucEthernetBuffer );
-            ( void ) pxInterface->pfOutput( pxInterface, pxNetworkBuffer, pdTRUE );
+            if( ( pxInterface != NULL ) && ( pxInterface->pfOutput != NULL ) )
+            {
+                ( void ) pxInterface->pfOutput( pxInterface, pxNetworkBuffer, pdTRUE );
+            }
         }
         else
         {

test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/Makefile.json

@@ -7,7 +7,9 @@
   [
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_UDP_IP.goto"
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_UDP_IP.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_UDP_IPv4.goto"
   ],
   "INSTFLAGS":
   [

test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c

@@ -75,11 +75,22 @@ eARPLookupResult_t eARPGetCacheEntry( uint32_t * pulIPAddress,
     return eResult;
 }
 
+BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDescriptor,
+                                                NetworkBufferDescriptor_t * const pxNetworkBuffer,
+                                                BaseType_t xReleaseAfterSend )
+{
+    __CPROVER_assert( pxDescriptor != NULL, "The network interface cannot be NULL." );
+    __CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." );
+    __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "The Ethernet buffer cannot be NULL." );
+    BaseType_t ret;
+    return ret;
+}
+
 
 void harness()
 {
     size_t xRequestedSizeBytes;
-
+    
     /* Assume that the size of packet must be greater than that of UDP-Packet and less than
      * that of the Ethernet Frame Size. */
     __CPROVER_assume( xRequestedSizeBytes >= sizeof( UDPPacket_t ) && xRequestedSizeBytes <= ipTOTAL_ETHERNET_FRAME_SIZE );
@@ -91,5 +102,35 @@ void harness()
     __CPROVER_assume( pxNetworkBuffer != NULL );
     __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
 
+    /*
+    Add an end point to the network buffer present. Its assumed that the
+    network interface layer correctly assigns the end point to the generated buffer.
+    */
+    pxNetworkBuffer->pxEndPoint = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkBuffer->pxEndPoint != NULL );
+    pxNetworkBuffer->pxEndPoint->pxNext = NULL;
+
+    /* Add an interface */
+    pxNetworkBuffer->pxEndPoint->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
+    __CPROVER_assume( pxNetworkBuffer->pxEndPoint->pxNetworkInterface != NULL );
+
+    /* Add few endpoints to global pxNetworkEndPoints */
+    pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkEndPoints != NULL );
+    pxNetworkEndPoints->pxNetworkInterface = pxNetworkBuffer->pxEndPoint->pxNetworkInterface;
+    if( nondet_bool() )
+    {
+        pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+        __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
+        pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkBuffer->pxEndPoint->pxNetworkInterface;
+        pxNetworkEndPoints->pxNext->pxNext = NULL;
+    }
+    else
+    {
+        pxNetworkEndPoints->pxNext = NULL;
+    }
+
+    pxNetworkBuffer->pxEndPoint->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub;
+
     vProcessGeneratedUDPPacket( pxNetworkBuffer );
 }

test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json

@@ -12,6 +12,7 @@
   [
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_UDP_IP.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_UDP_IPv4.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto"
   ],
   "DEF":

test/cbmc/stubs/freertos_api.c

@@ -212,7 +212,8 @@ int32_t FreeRTOS_sendto( Socket_t xSocket,
 ****************************************************************/
 
 void * FreeRTOS_GetUDPPayloadBuffer( size_t xRequestedSizeBytes,
-                                     TickType_t xBlockTimeTicks )
+                                     TickType_t xBlockTimeTicks,
+                                     uint8_t ucIPType )
 {
     size_t size;
 
@@ -225,7 +226,7 @@ void * FreeRTOS_GetUDPPayloadBuffer( size_t xRequestedSizeBytes,
 }
 
 /****************************************************************
-* Abstract FreeRTOS_GetUDPPayloadBuffer
+* Abstract FreeRTOS_ReleaseUDPPayloadBuffer
 * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/FreeRTOS_ReleaseUDPPayloadBuffer.html
 ****************************************************************/