[V4.3.2] Improve maximum network buffer allocation size check when Buffer Allocation scheme 1 is used (#1266)

tony-josi-aws · web-flow · commit d04851b7b92e · 2025-06-10T15:11:57.000+05:30
* Return allocated buffer size from vNetworkInterfaceAllocateRAMToBuffers and use it to verify allocation requests when using Buffer Allocation 1

* Rename vNetworkInterfaceAllocateRAMToBuffers to uxNetworkInterfaceAllocateRAMToBuffers

* Add min bytes assert for uxMaxNetworkInterfaceAllocatedSizeBytes

* Fix formatting

* Fix CBMC

* Fix formatting

* Address review comments

* Fix inconsistent definition for dmaRX_TX_BUFFER_SIZE for Xilinx ports

* Update allocation size for TM4C interface
diff --git a/source/include/NetworkInterface.h b/source/include/NetworkInterface.h
@@ -48,7 +48,7 @@
  */
 
 /* The following function is defined only when BufferAllocation_1.c is linked in the project. */
-void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] );
+size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] );
 
 BaseType_t xGetPhyLinkStatus( struct xNetworkInterface * pxInterface );
 
diff --git a/source/portable/BufferManagement/BufferAllocation_1.c b/source/portable/BufferManagement/BufferAllocation_1.c
@@ -70,6 +70,8 @@ static NetworkBufferDescriptor_t xNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DES
  * packet. No resizing will be done. */
 const BaseType_t xBufferAllocFixedSize = pdTRUE;
 
+static size_t uxMaxNetworkInterfaceAllocatedSizeBytes;
+
 /* The semaphore used to obtain network buffers. */
 static SemaphoreHandle_t xNetworkBufferSemaphore = NULL;
 
@@ -201,7 +203,10 @@ BaseType_t xNetworkBuffersInitialise( void )
             /* Initialise all the network buffers.  The buffer storage comes
              * from the network interface, and different hardware has different
              * requirements. */
-            vNetworkInterfaceAllocateRAMToBuffers( xNetworkBuffers );
+            uxMaxNetworkInterfaceAllocatedSizeBytes = uxNetworkInterfaceAllocateRAMToBuffers( xNetworkBuffers );
+
+            /* The allocated buffer should hold atleast ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER bytes */
+            configASSERT( ( uxMaxNetworkInterfaceAllocatedSizeBytes >= ( ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER ) ) );
 
             for( x = 0U; x < ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS; x++ )
             {
@@ -238,7 +243,7 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS
     UBaseType_t uxCount;
 
     if( ( xNetworkBufferSemaphore != NULL ) &&
-        ( xRequestedSizeBytes <= ( ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER ) ) )
+        ( xRequestedSizeBytes <= uxMaxNetworkInterfaceAllocatedSizeBytes ) )
     {
         /* If there is a semaphore available, there is a network buffer
          * available. */
@@ -429,7 +434,7 @@ UBaseType_t uxGetNumberOfFreeNetworkBuffers( void )
 NetworkBufferDescriptor_t * pxResizeNetworkBufferWithDescriptor( NetworkBufferDescriptor_t * pxNetworkBuffer,
                                                                  size_t xNewSizeBytes )
 {
-    if( xNewSizeBytes <= ( ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER ) )
+    if( xNewSizeBytes <= uxMaxNetworkInterfaceAllocatedSizeBytes )
     {
         /* In BufferAllocation_1.c all network buffer are allocated with a
          * maximum size of 'ipTOTAL_ETHERNET_FRAME_SIZE'.No need to resize the
diff --git a/source/portable/NetworkInterface/ATSAME5x/NetworkInterface.c b/source/portable/NetworkInterface/ATSAME5x/NetworkInterface.c
@@ -499,9 +499,10 @@ void xRxCallback( void )
 
 #if ( ipUSE_STATIC_ALLOCATION == 1 )
 
-/* Next provide the vNetworkInterfaceAllocateRAMToBuffers() function, which
- * simply fills in the pucEthernetBuffer member of each descriptor. */
-    void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
+/* Next provide the uxNetworkInterfaceAllocateRAMToBuffers() function, which
+ * simply fills in the pucEthernetBuffer member of each descriptor and returns
+ * the allocated buffer size. */
+    size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
     {
         BaseType_t x;
 
@@ -515,6 +516,8 @@ void xRxCallback( void )
              * future versions. */
             *( ( uint32_t * ) &ucBuffers[ x ][ 0 ] ) = ( uint32_t ) &( pxNetworkBuffers[ x ] );
         }
+
+        return( NETWORK_BUFFER_SIZE - ipBUFFER_PADDING );
     }
 #endif /* if ( ipUSE_STATIC_ALLOCATION == 1 ) */
 
diff --git a/source/portable/NetworkInterface/DriverSAM/NetworkInterface.c b/source/portable/NetworkInterface/DriverSAM/NetworkInterface.c
@@ -1409,7 +1409,7 @@ static void vCheckBuffersAndQueue( void )
 /*-----------------------------------------------------------*/
 
 extern uint8_t ucNetworkPackets[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS * NETWORK_BUFFER_SIZE ];
-void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
+size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
 {
     uint8_t * ucRAMBuffer = ucNetworkPackets;
     uint32_t ulIndex;
@@ -1422,6 +1422,8 @@ void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkB
     }
 
     cache_clean_invalidate();
+
+    return( NETWORK_BUFFER_SIZE - ipBUFFER_PADDING );
 }
 /*-----------------------------------------------------------*/
 
diff --git a/source/portable/NetworkInterface/LPC18xx/NetworkInterface.c b/source/portable/NetworkInterface/LPC18xx/NetworkInterface.c
@@ -332,7 +332,7 @@ BaseType_t xNetworkInterfaceInitialise( void )
 
 static __attribute__( ( section( "._ramAHB32" ) ) ) uint8_t ucNetworkPackets[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS * niBUFFER_1_PACKET_SIZE ] __attribute__( ( aligned( 32 ) ) );
 
-void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
+size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
 {
     uint8_t * ucRAMBuffer = ucNetworkPackets;
     uint32_t ul;
@@ -343,6 +343,8 @@ void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkB
         *( ( unsigned * ) ucRAMBuffer ) = ( unsigned ) ( &( pxNetworkBuffers[ ul ] ) );
         ucRAMBuffer += niBUFFER_1_PACKET_SIZE;
     }
+
+    return( niBUFFER_1_PACKET_SIZE - ipBUFFER_PADDING );
 }
 /*-----------------------------------------------------------*/
 
diff --git a/source/portable/NetworkInterface/LPC54018/NetworkInterface.c b/source/portable/NetworkInterface/LPC54018/NetworkInterface.c
@@ -372,11 +372,13 @@ BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxNetworkB
 /* statically allocate the buffers */
 /* allocating them as uint32_t's to force them into word alignment, a requirement of the DMA. */
 __ALIGN_BEGIN static uint32_t buffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ][ ( ipBUFFER_PADDING + ENET_RXBUFF_SIZE ) / sizeof( uint32_t ) + 1 ] __ALIGN_END;
-void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
+size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
 {
     for( int x = 0; x < ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS; x++ )
     {
         pxNetworkBuffers[ x ].pucEthernetBuffer = ( uint8_t * ) &buffers[ x ][ 0 ] + ipBUFFER_PADDING;
         buffers[ x ][ 0 ] = ( uint32_t ) &pxNetworkBuffers[ x ];
     }
+
+    return ENET_RXBUFF_SIZE;
 }
diff --git a/source/portable/NetworkInterface/M487/NetworkInterface.c b/source/portable/NetworkInterface/M487/NetworkInterface.c
@@ -180,7 +180,7 @@ BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxDescript
 }
 
 
-void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
+size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
 {
     uint8_t * ucRAMBuffer = ucNetworkPackets;
     uint32_t ul;
@@ -191,6 +191,8 @@ void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkB
         *( ( unsigned * ) ucRAMBuffer ) = ( unsigned ) ( &( pxNetworkBuffers[ ul ] ) );
         ucRAMBuffer += niBUFFER_1_PACKET_SIZE;
     }
+
+    return( niBUFFER_1_PACKET_SIZE - ipBUFFER_PADDING );
 }
 
 
diff --git a/source/portable/NetworkInterface/MPS2_AN385/NetworkInterface.c b/source/portable/NetworkInterface/MPS2_AN385/NetworkInterface.c
@@ -368,7 +368,7 @@ static BaseType_t xMPS2_NetworkInterfaceOutput( NetworkInterface_t * pxInterface
 }
 /*-----------------------------------------------------------*/
 
-void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
+size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
 {
     /* FIX ME if you want to use BufferAllocation_1.c, which uses statically
      * allocated network buffers. */
@@ -377,6 +377,7 @@ void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkB
      * without implementing this function. */
     configASSERT( xRxTaskHandle == ( TaskHandle_t ) 1 );
     ( void ) pxNetworkBuffers;
+    return 0;
 }
 /*-----------------------------------------------------------*/
 
diff --git a/source/portable/NetworkInterface/MPS3_AN552/NetworkInterface.c b/source/portable/NetworkInterface/MPS3_AN552/NetworkInterface.c
@@ -485,7 +485,7 @@ static BaseType_t xLAN91C111_NetworkInterfaceOutput( NetworkInterface_t * pxInte
 }
 /*-----------------------------------------------------------*/
 
-void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
+size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
 {
     /* FIX ME if you want to use BufferAllocation_1.c, which uses statically
      * allocated network buffers. */
@@ -494,6 +494,7 @@ void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkB
      * without implementing this function. */
     configASSERT( 0 );
     ( void ) pxNetworkBuffers;
+    return 0;
 }
 /*-----------------------------------------------------------*/
 
diff --git a/source/portable/NetworkInterface/MPS4_CS315/NetworkInterface.c b/source/portable/NetworkInterface/MPS4_CS315/NetworkInterface.c
@@ -485,7 +485,7 @@ static BaseType_t xLAN91C111_NetworkInterfaceOutput( NetworkInterface_t * pxInte
 }
 /*-----------------------------------------------------------*/
 
-void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
+size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
 {
     /* FIX ME if you want to use BufferAllocation_1.c, which uses statically
      * allocated network buffers. */
@@ -494,6 +494,7 @@ void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkB
      * without implementing this function. */
     configASSERT( 0 );
     ( void ) pxNetworkBuffers;
+    return 0;
 }
 /*-----------------------------------------------------------*/
 
diff --git a/source/portable/NetworkInterface/RX/NetworkInterface.c b/source/portable/NetworkInterface/RX/NetworkInterface.c
@@ -416,13 +416,13 @@ static void prvEMACDeferredInterruptHandlerTask( void * pvParameters )
 
 
 /***********************************************************************************************************************
- * Function Name: vNetworkInterfaceAllocateRAMToBuffers ()
+ * Function Name: uxNetworkInterfaceAllocateRAMToBuffers ()
  * Description  : .
  * Arguments    : pxNetworkBuffers
  * Return Value : none
  **********************************************************************************************************************/
 
-void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
+size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
 {
     uint32_t ul;
     uint8_t * buffer_address;
@@ -443,7 +443,9 @@ void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkB
         *( ( unsigned * ) buffer_address ) = ( unsigned ) ( &( pxNetworkBuffers[ ul ] ) );
         buffer_address += ETHER_CFG_BUFSIZE;
     }
-} /* End of function vNetworkInterfaceAllocateRAMToBuffers() */
+
+    return( ETHER_CFG_BUFSIZE - ipBUFFER_PADDING );
+} /* End of function uxNetworkInterfaceAllocateRAMToBuffers() */
 
 /***********************************************************************************************************************
  * Function Name: prvLinkStatusChange ()
diff --git a/source/portable/NetworkInterface/STM32/Legacy/STM32Fxx/NetworkInterface.c b/source/portable/NetworkInterface/STM32/Legacy/STM32Fxx/NetworkInterface.c
@@ -1377,7 +1377,7 @@ static BaseType_t xSTM32F_GetPhyLinkStatus( NetworkInterface_t * pxInterface )
 
 /* Uncomment this in case BufferAllocation_1.c is used. */
 
-void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
+size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
 {
     static
     #if defined( STM32F7xx )
@@ -1393,6 +1393,7 @@ void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkB
         *( ( unsigned * ) ucRAMBuffer ) = ( unsigned ) ( &( pxNetworkBuffers[ ul ] ) );
         ucRAMBuffer += ETH_MAX_PACKET_SIZE;
     }
+    return (ETH_MAX_PACKET_SIZE - ipBUFFER_PADDING);
 }
 
 /*-----------------------------------------------------------*/
diff --git a/source/portable/NetworkInterface/STM32/Legacy/STM32Hxx/NetworkInterface.c b/source/portable/NetworkInterface/STM32/Legacy/STM32Hxx/NetworkInterface.c
@@ -1034,7 +1034,7 @@ uint8_t ucNetworkPackets[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS * ETH_RX_BUF_SI
 #endif /* ( ipconfigZERO_COPY_RX_DRIVER != 0 || ipconfigZERO_COPY_TX_DRIVER != 0 ) */
 __attribute__( ( aligned( 32 ) ) );
 
-void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
+size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
 {
     uint8_t * ucRAMBuffer = ucNetworkPackets;
     uint32_t ul;
@@ -1045,6 +1045,8 @@ void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkB
         *( ( unsigned * ) ucRAMBuffer ) = ( unsigned ) ( &( pxNetworkBuffers[ ul ] ) );
         ucRAMBuffer += ETH_RX_BUF_SIZE;
     }
+
+    return (ETH_RX_BUF_SIZE - ipBUFFER_PADDING);
 }
 /*-----------------------------------------------------------*/
 
diff --git a/source/portable/NetworkInterface/STM32/NetworkInterface.c b/source/portable/NetworkInterface/STM32/NetworkInterface.c
@@ -1971,7 +1971,7 @@ void HAL_ETH_TxFreeCallback( uint32_t * pulBuff )
 /*===========================================================================*/
 /*---------------------------------------------------------------------------*/
 
-void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
+size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
 {
     static uint8_t ucNetworkPackets[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ][ niEMAC_TOTAL_BUFFER_SIZE ] __ALIGNED( niEMAC_BUF_ALIGNMENT ) __attribute__( ( section( niEMAC_BUFFERS_SECTION ) ) );
 
@@ -1985,6 +1985,8 @@ void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkB
         pxNetworkBuffers[ uxIndex ].pucEthernetBuffer = &( ucNetworkPackets[ uxIndex ][ ipBUFFER_PADDING ] );
         *( ( uint32_t * ) &( ucNetworkPackets[ uxIndex ][ 0 ] ) ) = ( uint32_t ) ( &( pxNetworkBuffers[ uxIndex ] ) );
     }
+
+    return (niEMAC_TOTAL_BUFFER_SIZE - ipBUFFER_PADDING);
 }
 
 /*---------------------------------------------------------------------------*/
diff --git a/source/portable/NetworkInterface/TM4C/NetworkInterface.c b/source/portable/NetworkInterface/TM4C/NetworkInterface.c
@@ -57,7 +57,7 @@
 #include "NetworkInterface.h"
 #include "phyHandling.h"
 
-#define BUFFER_SIZE_WO_PADDING     ( ipconfigNETWORK_MTU + ipSIZE_OF_ETH_HEADER )
+#define BUFFER_SIZE_WO_PADDING     ( ipTOTAL_ETHERNET_FRAME_SIZE )
 #define BUFFER_SIZE                ( BUFFER_SIZE_WO_PADDING + ipBUFFER_PADDING )
 #define BUFFER_SIZE_ROUNDED_UP     ( ( BUFFER_SIZE + 7 ) & ~0x7UL )
 #define PHY_PHYS_ADDR              0
@@ -403,7 +403,7 @@ BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxNetworkB
     return success;
 }
 
-void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
+void uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
 {
     BaseType_t i;
 
@@ -415,6 +415,8 @@ void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkB
         /* Set the 'hidden' reference to the descriptor for use in DMA interrupts */
         *( ( uint32_t * ) &_network_buffers[ i ][ 0 ] ) = ( uint32_t ) &( ( pxNetworkBuffers[ i ] ) );
     }
+
+    return( BUFFER_SIZE_ROUNDED_UP - ipBUFFER_PADDING );
 }
 
 static BaseType_t _ethernet_mac_get( uint8_t * mac_address_bytes )
diff --git a/source/portable/NetworkInterface/ThirdParty/MSP432/NetworkInterface.c b/source/portable/NetworkInterface/ThirdParty/MSP432/NetworkInterface.c
@@ -997,7 +997,7 @@ BaseType_t xGetPhyLinkStatus( void )
 #define BUFFER_SIZE_ALLOC1               ( ipTOTAL_ETHERNET_FRAME_SIZE + ipBUFFER_PADDING )
 #define BUFFER_SIZE_ALLOC1_ROUNDED_UP    ( ( BUFFER_SIZE_ALLOC1 + 7 ) & ~0x07UL )
 static uint8_t ucBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ][ BUFFER_SIZE_ALLOC1_ROUNDED_UP ];
-void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
+size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
 {
     BaseType_t x;
 
@@ -1011,4 +1011,6 @@ void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkB
          * future versions. */
         *( ( uint32_t * ) &ucBuffers[ x ][ 0 ] ) = ( uint32_t ) &( pxNetworkBuffers[ x ] );
     }
+
+    return( BUFFER_SIZE_ALLOC1_ROUNDED_UP - ipBUFFER_PADDING );
 }
diff --git a/source/portable/NetworkInterface/WinPCap/NetworkInterface.c b/source/portable/NetworkInterface/WinPCap/NetworkInterface.c
@@ -946,7 +946,7 @@ static const char * prvRemoveSpaces( char * pcBuffer,
 #define BUFFER_SIZE               ( ipTOTAL_ETHERNET_FRAME_SIZE + ipBUFFER_PADDING )
 #define BUFFER_SIZE_ROUNDED_UP    ( ( BUFFER_SIZE + 7 ) & ~0x07UL )
 
-void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
+size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
 {
     static uint8_t * pucNetworkPacketBuffers = NULL;
     size_t uxIndex;
@@ -979,4 +979,6 @@ void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkB
             pxNetworkBuffers[ uxIndex ].pucEthernetBuffer = &( pucNetworkPacketBuffers[ uxOffset + ipBUFFER_PADDING ] );
         }
     }
+
+    return( BUFFER_SIZE_ROUNDED_UP - ipBUFFER_PADDING );
 }
diff --git a/source/portable/NetworkInterface/Zynq/NetworkInterface.c b/source/portable/NetworkInterface/Zynq/NetworkInterface.c
@@ -486,7 +486,7 @@ static BaseType_t prvGMACWaitLS( BaseType_t xEMACIndex,
 /*-----------------------------------------------------------*/
 
 #if ( nicUSE_UNCACHED_MEMORY == 0 )
-    void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
+    size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
     {
         static uint8_t ucNetworkPackets[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS * niBUFFER_1_PACKET_SIZE ] __attribute__( ( aligned( 32 ) ) );
         uint8_t * ucRAMBuffer = ucNetworkPackets;
@@ -498,9 +498,11 @@ static BaseType_t prvGMACWaitLS( BaseType_t xEMACIndex,
             *( ( unsigned * ) ucRAMBuffer ) = ( unsigned ) ( &( pxNetworkBuffers[ ul ] ) );
             ucRAMBuffer += niBUFFER_1_PACKET_SIZE;
         }
+
+        return( niBUFFER_1_PACKET_SIZE - ipBUFFER_PADDING );
     }
 #else /* if ( nicUSE_UNCACHED_MEMORY == 0 ) */
-    void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
+    size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
     {
         static uint8_t * pucNetworkPackets = NULL;
 
@@ -521,6 +523,8 @@ static BaseType_t prvGMACWaitLS( BaseType_t xEMACIndex,
                 }
             }
         }
+
+        return( niBUFFER_1_PACKET_SIZE - ipBUFFER_PADDING );
     }
 #endif /* ( nicUSE_UNCACHED_MEMORY == 0 ) */
 /*-----------------------------------------------------------*/
diff --git a/source/portable/NetworkInterface/Zynq/x_emacpsif_dma.c b/source/portable/NetworkInterface/Zynq/x_emacpsif_dma.c
@@ -89,7 +89,7 @@
 #endif
 #define TX_OFFSET               ipconfigPACKET_FILLER_SIZE
 
-#define dmaRX_TX_BUFFER_SIZE    1536
+#define dmaRX_TX_BUFFER_SIZE    ( 1536 - ipBUFFER_PADDING )
 
 /* Defined in NetworkInterface.c */
 extern TaskHandle_t xEMACTaskHandles[ XPAR_XEMACPS_NUM_INSTANCES ];
diff --git a/source/portable/NetworkInterface/board_family/NetworkInterface.c b/source/portable/NetworkInterface/board_family/NetworkInterface.c
@@ -64,9 +64,10 @@ BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxNetworkB
     return pdFALSE;
 }
 
-void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
+size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )
 {
     /* FIX ME. */
+    return 0;
 }
 
 BaseType_t xGetPhyLinkStatus( void )
diff --git a/source/portable/NetworkInterface/libslirp/MBuffNetworkInterface.c b/source/portable/NetworkInterface/libslirp/MBuffNetworkInterface.c
diff --git a/source/portable/NetworkInterface/linux/NetworkInterface.c b/source/portable/NetworkInterface/linux/NetworkInterface.c
diff --git a/source/portable/NetworkInterface/mw300_rd/NetworkInterface.c b/source/portable/NetworkInterface/mw300_rd/NetworkInterface.c
diff --git a/source/portable/NetworkInterface/xilinx_ultrascale/NetworkInterface.c b/source/portable/NetworkInterface/xilinx_ultrascale/NetworkInterface.c
diff --git a/source/portable/NetworkInterface/xilinx_ultrascale/x_emacpsif_dma.c b/source/portable/NetworkInterface/xilinx_ultrascale/x_emacpsif_dma.c
diff --git a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json
diff --git a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c
diff --git a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/README.md b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/README.md
diff --git a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json
diff --git a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/README.md b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/README.md

Original file line number	Diff line number	Diff line change
`@@ -499,9 +499,10 @@ void xRxCallback( void )`
`499`	`499`
`500`	`500`	`#if ( ipUSE_STATIC_ALLOCATION == 1 )`
`501`	`501`
`502`		`-/* Next provide the vNetworkInterfaceAllocateRAMToBuffers() function, which`
`503`		`- * simply fills in the pucEthernetBuffer member of each descriptor. */`
`504`		`- void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )`
	`502`	`+/* Next provide the uxNetworkInterfaceAllocateRAMToBuffers() function, which`
	`503`	`+ * simply fills in the pucEthernetBuffer member of each descriptor and returns`
	`504`	`+ * the allocated buffer size. */`
	`505`	`+ size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )`
`505`	`506`	`{`
`506`	`507`	`BaseType_t x;`
`507`	`508`
`@@ -515,6 +516,8 @@ void xRxCallback( void )`
`515`	`516`	`* future versions. */`
`516`	`517`	`( ( uint32_t ) &ucBuffers[ x ][ 0 ] ) = ( uint32_t ) &( pxNetworkBuffers[ x ] );`
`517`	`518`	`}`
	`519`	`+`
	`520`	`+ return( NETWORK_BUFFER_SIZE - ipBUFFER_PADDING );`
`518`	`521`	`}`
`519`	`522`	`#endif /* if ( ipUSE_STATIC_ALLOCATION == 1 ) */`
`520`	`523`
Original file line number	Diff line number	Diff line change
`@@ -1409,7 +1409,7 @@ static void vCheckBuffersAndQueue( void )`
`1409`	`1409`	`/-----------------------------------------------------------/`
`1410`	`1410`
`1411`	`1411`	`extern uint8_t ucNetworkPackets[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS * NETWORK_BUFFER_SIZE ];`
`1412`		`-void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )`
	`1412`	`+size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )`
`1413`	`1413`	`{`
`1414`	`1414`	`uint8_t * ucRAMBuffer = ucNetworkPackets;`
`1415`	`1415`	`uint32_t ulIndex;`
`@@ -1422,6 +1422,8 @@ void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkB`
`1422`	`1422`	`}`
`1423`	`1423`
`1424`	`1424`	`cache_clean_invalidate();`
	`1425`	`+`
	`1426`	`+ return( NETWORK_BUFFER_SIZE - ipBUFFER_PADDING );`
`1425`	`1427`	`}`
`1426`	`1428`	`/-----------------------------------------------------------/`
`1427`	`1429`
Original file line number	Diff line number	Diff line change
`@@ -332,7 +332,7 @@ BaseType_t xNetworkInterfaceInitialise( void )`
`332`	`332`
`333`	`333`	`static __attribute__( ( section( "._ramAHB32" ) ) ) uint8_t ucNetworkPackets[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS * niBUFFER_1_PACKET_SIZE ] __attribute__( ( aligned( 32 ) ) );`
`334`	`334`
`335`		`-void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )`
	`335`	`+size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )`
`336`	`336`	`{`
`337`	`337`	`uint8_t * ucRAMBuffer = ucNetworkPackets;`
`338`	`338`	`uint32_t ul;`
`@@ -343,6 +343,8 @@ void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkB`
`343`	`343`	`( ( unsigned ) ucRAMBuffer ) = ( unsigned ) ( &( pxNetworkBuffers[ ul ] ) );`
`344`	`344`	`ucRAMBuffer += niBUFFER_1_PACKET_SIZE;`
`345`	`345`	`}`
	`346`	`+`
	`347`	`+ return( niBUFFER_1_PACKET_SIZE - ipBUFFER_PADDING );`
`346`	`348`	`}`
`347`	`349`	`/-----------------------------------------------------------/`
`348`	`350`
Original file line number	Diff line number	Diff line change
`@@ -372,11 +372,13 @@ BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxNetworkB`
`372`	`372`	`/* statically allocate the buffers */`
`373`	`373`	`/* allocating them as uint32_t's to force them into word alignment, a requirement of the DMA. */`
`374`	`374`	`__ALIGN_BEGIN static uint32_t buffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ][ ( ipBUFFER_PADDING + ENET_RXBUFF_SIZE ) / sizeof( uint32_t ) + 1 ] __ALIGN_END;`
`375`		`-void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )`
	`375`	`+size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )`
`376`	`376`	`{`
`377`	`377`	`for( int x = 0; x < ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS; x++ )`
`378`	`378`	`{`
`379`	`379`	`pxNetworkBuffers[ x ].pucEthernetBuffer = ( uint8_t * ) &buffers[ x ][ 0 ] + ipBUFFER_PADDING;`
`380`	`380`	`buffers[ x ][ 0 ] = ( uint32_t ) &pxNetworkBuffers[ x ];`
`381`	`381`	`}`
	`382`	`+`
	`383`	`+ return ENET_RXBUFF_SIZE;`
`382`	`384`	`}`
Original file line number	Diff line number	Diff line change
`@@ -180,7 +180,7 @@ BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxDescript`
`180`	`180`	`}`
`181`	`181`
`182`	`182`
`183`		`-void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )`
	`183`	`+size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )`
`184`	`184`	`{`
`185`	`185`	`uint8_t * ucRAMBuffer = ucNetworkPackets;`
`186`	`186`	`uint32_t ul;`
`@@ -191,6 +191,8 @@ void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkB`
`191`	`191`	`( ( unsigned ) ucRAMBuffer ) = ( unsigned ) ( &( pxNetworkBuffers[ ul ] ) );`
`192`	`192`	`ucRAMBuffer += niBUFFER_1_PACKET_SIZE;`
`193`	`193`	`}`
	`194`	`+`
	`195`	`+ return( niBUFFER_1_PACKET_SIZE - ipBUFFER_PADDING );`
`194`	`196`	`}`
`195`	`197`
`196`	`198`
Original file line number	Diff line number	Diff line change
`@@ -368,7 +368,7 @@ static BaseType_t xMPS2_NetworkInterfaceOutput( NetworkInterface_t * pxInterface`
`368`	`368`	`}`
`369`	`369`	`/-----------------------------------------------------------/`
`370`	`370`
`371`		`-void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )`
	`371`	`+size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )`
`372`	`372`	`{`
`373`	`373`	`/* FIX ME if you want to use BufferAllocation_1.c, which uses statically`
`374`	`374`	`* allocated network buffers. */`
`@@ -377,6 +377,7 @@ void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkB`
`377`	`377`	`* without implementing this function. */`
`378`	`378`	`configASSERT( xRxTaskHandle == ( TaskHandle_t ) 1 );`
`379`	`379`	`( void ) pxNetworkBuffers;`
	`380`	`+ return 0;`
`380`	`381`	`}`
`381`	`382`	`/-----------------------------------------------------------/`
`382`	`383`
Original file line number	Diff line number	Diff line change
`@@ -485,7 +485,7 @@ static BaseType_t xLAN91C111_NetworkInterfaceOutput( NetworkInterface_t * pxInte`
`485`	`485`	`}`
`486`	`486`	`/-----------------------------------------------------------/`
`487`	`487`
`488`		`-void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )`
	`488`	`+size_t uxNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkBuffers[ ipconfigNUM_NETWORK_BUFFER_DESCRIPTORS ] )`
`489`	`489`	`{`
`490`	`490`	`/* FIX ME if you want to use BufferAllocation_1.c, which uses statically`
`491`	`491`	`* allocated network buffers. */`
`@@ -494,6 +494,7 @@ void vNetworkInterfaceAllocateRAMToBuffers( NetworkBufferDescriptor_t pxNetworkB`
`494`	`494`	`* without implementing this function. */`
`495`	`495`	`configASSERT( 0 );`
`496`	`496`	`( void ) pxNetworkBuffers;`
	`497`	`+ return 0;`
`497`	`498`	`}`
`498`	`499`	`/-----------------------------------------------------------/`
`499`	`500`