From f5ce78e6753be1cee23fb6aed0c085795e0597b5 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 10 May 2024 17:30:53 +0000
Subject: [PATCH 01/36] CBMC: replace any missing functions by assert-false

---
 test/cbmc/proofs/Makefile.template | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/test/cbmc/proofs/Makefile.template b/test/cbmc/proofs/Makefile.template
index 094fd560c..15cf815db 100644
--- a/test/cbmc/proofs/Makefile.template
+++ b/test/cbmc/proofs/Makefile.template
@@ -105,7 +105,11 @@ $(ENTRY)5.goto: $(ENTRY)4.goto
 	$(GOTO_INSTRUMENT) --drop-unused-functions @RULE_INPUT@ @RULE_OUTPUT@ \
 		> $(ENTRY)5.txt 2>&1
 
-$(ENTRY).goto: $(ENTRY)5.goto
+$(ENTRY)6.goto: $(ENTRY)5.goto
+	$(GOTO_INSTRUMENT) --generate-function-body '(?!__CPROVER).*' --generate-function-body-options assert-false @RULE_INPUT@ @RULE_OUTPUT@ \
+		> $(ENTRY)6.txt 2>&1
+
+$(ENTRY).goto: $(ENTRY)6.goto
 	@CP@ @RULE_INPUT@ @RULE_OUTPUT@
 
 # ____________________________________________________________________

From 8d9b79d5a5d2931c18399d9cc4dfa2794a71efe4 Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Mon, 8 Jul 2024 08:11:27 +0000
Subject: [PATCH 02/36] Fix ARPAgeCache CBMC test

---
 .../ARP/ARPAgeCache/ARPAgeCache_harness.c       |  6 ++++++
 test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json  |  3 +++
 test/cbmc/stubs/freertos_kernel_api.c           | 17 +++++++++++++++++
 3 files changed, 26 insertions(+)

diff --git a/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c b/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c
index 5a5b3e7c2..509cacb7b 100644
--- a/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c
+++ b/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c
@@ -33,6 +33,12 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes
     return 0;
 }
 
+
+void FreeRTOS_OutputAdvertiseIPv6( NetworkEndPoint_t * pxEndPoint )
+{
+    __CPROVER_assert( pxEndPoint != NULL, "The Endpoint cannot be NULL." );
+}
+
 void harness()
 {
     /*
diff --git a/test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json b/test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json
index 24de2ff3c..b122ddc7d 100644
--- a/test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json
+++ b/test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json
@@ -15,6 +15,9 @@
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
     "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto"
   ],
   "DEF":
diff --git a/test/cbmc/stubs/freertos_kernel_api.c b/test/cbmc/stubs/freertos_kernel_api.c
index b74b4ec09..87cff0bac 100644
--- a/test/cbmc/stubs/freertos_kernel_api.c
+++ b/test/cbmc/stubs/freertos_kernel_api.c
@@ -80,3 +80,20 @@ EventBits_t xEventGroupSetBits( EventGroupHandle_t xEventGroup,
 }
 
 /****************************************************************/
+
+/****************************************************************
+* Abstract xQueueGenericSend
+****************************************************************/
+BaseType_t xQueueGenericSend( QueueHandle_t xQueue,
+                              const void * const pvItemToQueue,
+                              TickType_t xTicksToWait,
+                              const BaseType_t xCopyPosition )
+{
+    BaseType_t xReturn;
+
+    __CPROVER_assume( ( xReturn == pdTRUE ) || ( xReturn == pdFALSE ) );
+
+    return xReturn;
+}
+
+/****************************************************************/

From 11ac0caab409bc41459ec50293c8d51ff4fa1088 Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Tue, 9 Jul 2024 04:18:17 +0000
Subject: [PATCH 03/36] Fix eARPProcessPacket CBMC test

---
 .../ARP/ARPGetCacheEntry/Configurations.json  |  2 +
 .../ARPProcessPacket_harness.c                | 85 ++++++++++++-------
 .../proofs/ARP/ARPProcessPacket/Makefile.json |  5 +-
 test/cbmc/stubs/freertos_api.c                | 10 +++
 test/cbmc/stubs/freertos_kernel_api.c         | 36 ++++++++
 5 files changed, 106 insertions(+), 32 deletions(-)

diff --git a/test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json b/test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json
index aa4d60296..3301afb40 100644
--- a/test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json
+++ b/test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json
@@ -14,6 +14,8 @@
   [
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IPv4.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IPv4_Utils.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto"
   ],
   "DEF":
diff --git a/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c b/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
index 539f02d18..7be804559 100644
--- a/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
+++ b/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
@@ -1,5 +1,3 @@
-#include "cbmc.h"
-
 /* FreeRTOS includes. */
 #include "FreeRTOS.h"
 #include "queue.h"
@@ -10,8 +8,37 @@
 #include "FreeRTOS_ARP.h"
 #include "FreeRTOS_Routing.h"
 
+/* CBMC includes. */
+#include "cbmc.h"
+
 /* This pointer is maintained by the IP-task. Defined in FreeRTOS_IP.c */
 extern NetworkBufferDescriptor_t * pxARPWaitingNetworkBuffer;
+NetworkEndPoint_t * pxNetworkEndPoint_Temp;
+
+/* Stub FreeRTOS_FindEndPointOnNetMask_IPv6 as its not relevant to the
+ * correctness of the proof */
+NetworkEndPoint_t * FreeRTOS_FindEndPointOnNetMask_IPv6( const IPv6_Address_t * pxIPv6Address )
+{
+    __CPROVER_assert( pxIPv6Address != NULL, "Precondition: pxIPv6Address != NULL" );
+
+    /* Assume at least one end-point is available */
+    return pxNetworkEndPoint_Temp;
+}
+
+/* Stub FreeRTOS_FindEndPointOnNetMask_IPv6 as its not relevant to the
+ * correctness of the proof */
+NetworkEndPoint_t * FreeRTOS_FindEndPointOnNetMask( uint32_t ulIPAddress,
+                                                    uint32_t ulWhere )
+{
+    /* Assume at least one end-point is available */
+    return pxNetworkEndPoint_Temp;
+}
+
+/* Get rid of configASSERT in FreeRTOS_TCP_IP.c */
+BaseType_t xIsCallingFromIPTask( void )
+{
+    return pdTRUE;
+}
 
 /* This is an output function and need not be tested with this proof. */
 void FreeRTOS_OutputARPRequest_Multi( NetworkEndPoint_t * pxEndPoint,
@@ -36,9 +63,19 @@ eARPLookupResult_t eARPGetCacheEntry( uint32_t * pulIPAddress,
 
 void harness()
 {
-    NetworkBufferDescriptor_t xLocalBuffer;
+    NetworkBufferDescriptor_t * pxLocalBuffer;
+    NetworkBufferDescriptor_t * pxNetworkBuffer2;
+    TickType_t xBlockTimeTicks;
     uint16_t usEthernetBufferSize;
 
+    /*
+     * The assumption made here is that the buffer pointed by pucEthernetBuffer
+     * is at least allocated to sizeof(ARPPacket_t) size but eventually an even larger buffer.
+     * This is not checked inside eARPProcessPacket.
+     */
+    uint8_t ucBUFFER_SIZE;
+
+
     /* Non deterministically determine whether the pxARPWaitingNetworkBuffer will
      * point to some valid data or will it be NULL. */
     if( nondet_bool() )
@@ -47,48 +84,34 @@ void harness()
          * checked in the function as the pointer is stored by the IP-task itself
          * and therefore it will always be of the required size. */
         __CPROVER_assume( usEthernetBufferSize >= sizeof( IPPacket_t ) );
-
-        /* Add matching data length to the network buffer descriptor. */
-        __CPROVER_assume( xLocalBuffer.xDataLength == usEthernetBufferSize );
-
-        xLocalBuffer.pucEthernetBuffer = malloc( usEthernetBufferSize );
+        pxLocalBuffer = pxGetNetworkBufferWithDescriptor( usEthernetBufferSize, xBlockTimeTicks );
 
         /* Since this pointer is maintained by the IP-task, either the pointer
-         * pxARPWaitingNetworkBuffer will be NULL or xLocalBuffer.pucEthernetBuffer
+         * pxARPWaitingNetworkBuffer will be NULL or pxLocalBuffer->pucEthernetBuffer
          * will be non-NULL. */
-        __CPROVER_assume( xLocalBuffer.pucEthernetBuffer != NULL );
+        __CPROVER_assume( pxLocalBuffer != NULL );
+        __CPROVER_assume( pxLocalBuffer->pucEthernetBuffer != NULL );
+        __CPROVER_assume( pxLocalBuffer->xDataLength == usEthernetBufferSize );
 
-        pxARPWaitingNetworkBuffer = &xLocalBuffer;
+        pxARPWaitingNetworkBuffer = pxLocalBuffer;
     }
     else
     {
         pxARPWaitingNetworkBuffer = NULL;
     }
 
-    /*
-     * The assumption made here is that the buffer pointed by pucEthernetBuffer
-     * is at least allocated to sizeof(ARPPacket_t) size but eventually an even larger buffer.
-     * This is not checked inside eARPProcessPacket.
-     */
-    uint8_t ucBUFFER_SIZE;
-
-    void * xBuffer = malloc( ucBUFFER_SIZE + sizeof( ARPPacket_t ) );
-
-    __CPROVER_assume( xBuffer != NULL );
-
-    NetworkBufferDescriptor_t xNetworkBuffer2;
-
-    xNetworkBuffer2.pucEthernetBuffer = xBuffer;
-    xNetworkBuffer2.xDataLength = ucBUFFER_SIZE + sizeof( ARPPacket_t );
+    pxNetworkBuffer2 = pxGetNetworkBufferWithDescriptor( ucBUFFER_SIZE + sizeof( ARPPacket_t ), xBlockTimeTicks );
+    __CPROVER_assume( pxNetworkBuffer2 != NULL );
+    __CPROVER_assume( pxNetworkBuffer2->pucEthernetBuffer != NULL );
 
     /*
      * This proof assumes one end point is present.
      */
-    xNetworkBuffer2.pxEndPoint = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
-    __CPROVER_assume( xNetworkBuffer2.pxEndPoint != NULL );
-    xNetworkBuffer2.pxEndPoint->pxNext = NULL;
+    pxNetworkBuffer2->pxEndPoint = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkBuffer2->pxEndPoint != NULL );
+    pxNetworkBuffer2->pxEndPoint->pxNext = NULL;
 
     /* eARPProcessPacket will be called in the source code only after checking if
-     * xNetworkBuffer2.pucEthernetBuffer is not NULL, hence, __CPROVER_assume( xBuffer != NULL );   */
-    eARPProcessPacket( &xNetworkBuffer2 );
+     * pxNetworkBuffer2->pucEthernetBuffer is not NULL, hence, __CPROVER_assume( xBuffer != NULL );   */
+    eARPProcessPacket( pxNetworkBuffer2 );
 }
diff --git a/test/cbmc/proofs/ARP/ARPProcessPacket/Makefile.json b/test/cbmc/proofs/ARP/ARPProcessPacket/Makefile.json
index 00079ded1..003611ae9 100644
--- a/test/cbmc/proofs/ARP/ARPProcessPacket/Makefile.json
+++ b/test/cbmc/proofs/ARP/ARPProcessPacket/Makefile.json
@@ -11,6 +11,9 @@
   [
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto"
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto"
   ]
 }
diff --git a/test/cbmc/stubs/freertos_api.c b/test/cbmc/stubs/freertos_api.c
index d541aa07a..cc13622c6 100644
--- a/test/cbmc/stubs/freertos_api.c
+++ b/test/cbmc/stubs/freertos_api.c
@@ -388,3 +388,13 @@ BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxNetworkB
 }
 
 /****************************************************************/
+
+/****************************************************************
+* Abstract vIPSetARPResolutionTimerEnableState
+****************************************************************/
+void vIPSetARPResolutionTimerEnableState( BaseType_t xEnableState )
+{
+
+}
+
+/****************************************************************/
diff --git a/test/cbmc/stubs/freertos_kernel_api.c b/test/cbmc/stubs/freertos_kernel_api.c
index 87cff0bac..25ea16dd6 100644
--- a/test/cbmc/stubs/freertos_kernel_api.c
+++ b/test/cbmc/stubs/freertos_kernel_api.c
@@ -97,3 +97,39 @@ BaseType_t xQueueGenericSend( QueueHandle_t xQueue,
 }
 
 /****************************************************************/
+
+/****************************************************************
+* Abstract vTaskSetTimeOutState
+****************************************************************/
+void vTaskSetTimeOutState( TimeOut_t * const pxTimeOut )
+{
+}
+
+/****************************************************************/
+
+/****************************************************************
+* Abstract xTaskCheckForTimeOut
+****************************************************************/
+BaseType_t xTaskCheckForTimeOut( TimeOut_t * const pxTimeOut,
+                                 TickType_t * const pxTicksToWait )
+{
+    BaseType_t xReturn;
+
+    __CPROVER_assume( ( xReturn == pdTRUE ) || ( xReturn == pdFALSE ) );
+
+    return xReturn;
+}
+
+/****************************************************************/
+
+/****************************************************************
+* Abstract xTaskGetTickCount
+****************************************************************/
+TickType_t xTaskGetTickCount( void )
+{
+    TickType_t xReturn;
+
+    return xReturn;
+}
+
+/****************************************************************/

From e4f9205df76efc9f58830d3235e0ed44770656f7 Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Tue, 9 Jul 2024 04:20:48 +0000
Subject: [PATCH 04/36] Fix ARPSendGratuitous CBMC test

---
 test/cbmc/proofs/ARP/ARPSendGratuitous/Makefile.json | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/test/cbmc/proofs/ARP/ARPSendGratuitous/Makefile.json b/test/cbmc/proofs/ARP/ARPSendGratuitous/Makefile.json
index f069f5959..044a2b2c2 100644
--- a/test/cbmc/proofs/ARP/ARPSendGratuitous/Makefile.json
+++ b/test/cbmc/proofs/ARP/ARPSendGratuitous/Makefile.json
@@ -10,7 +10,9 @@
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
-    "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto"
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto",
+    "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto"
   ],
   "DEF":
   [

From cbbcc4f911988877e886eefd1c6c001e8728c49d Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Tue, 9 Jul 2024 07:20:21 +0000
Subject: [PATCH 05/36] Fix ARP_FreeRTOS_OutputARPRequest CBMC test

---
 .../Configurations.json                       |  4 +-
 .../OutputARPRequest_harness.c                | 37 ++++++++++++++++---
 2 files changed, 34 insertions(+), 7 deletions(-)

diff --git a/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json b/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json
index 62bb3e052..5e2c516c3 100644
--- a/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json
+++ b/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json
@@ -37,7 +37,9 @@
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto"
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto"
   ],
   #That is the minimal required size for an ARPPacket_t plus offset in the buffer.
   "MINIMUM_PACKET_BYTES": 50,
diff --git a/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c b/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c
index 9337fb4f7..b5b45cf67 100644
--- a/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c
+++ b/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c
@@ -35,6 +35,8 @@
 #include "FreeRTOS_IP_Private.h"
 #include "FreeRTOS_ARP.h"
 
+/* CBMC includes. */
+#include "cbmc.h"
 
 ARPPacket_t xARPPacket;
 NetworkBufferDescriptor_t xNetworkBuffer;
@@ -56,15 +58,15 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS
 {
     #ifdef CBMC_PROOF_ASSUMPTION_HOLDS
         #if ( ipconfigETHERNET_MINIMUM_PACKET_BYTES > 0 )
-            xNetworkBuffer.pucEthernetBuffer = malloc( ipconfigETHERNET_MINIMUM_PACKET_BYTES );
+            xNetworkBuffer.pucEthernetBuffer = safeMalloc( ipconfigETHERNET_MINIMUM_PACKET_BYTES );
         #else
-            xNetworkBuffer.pucEthernetBuffer = malloc( xRequestedSizeBytes );
+            xNetworkBuffer.pucEthernetBuffer = safeMalloc( xRequestedSizeBytes );
         #endif
     #else
         uint32_t malloc_size;
         __CPROVER_assert( !__CPROVER_overflow_mult( 2, xRequestedSizeBytes ) );
         __CPROVER_assume( malloc_size > 0 && malloc_size < 2 * xRequestedSizeBytes );
-        xNetworkBuffer.pucEthernetBuffer = malloc( malloc_size );
+        xNetworkBuffer.pucEthernetBuffer = safeMalloc( malloc_size );
     #endif
     __CPROVER_assume( xNetworkBuffer.pucEthernetBuffer != NULL );
 
@@ -72,6 +74,21 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS
     return &xNetworkBuffer;
 }
 
+/* STUB!
+ * In this function, it only allocates network buffer by pxGetNetworkBufferWithDescriptor
+ * stub function above here. In this case, we should just free the allocated pucEthernetBuffer.
+ */
+void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer )
+{
+    __CPROVER_assert( pxNetworkBuffer != NULL,
+                      "Precondition: pxNetworkBuffer != NULL" );
+
+    if( pxNetworkBuffer->pucEthernetBuffer != NULL )
+    {
+        free( pxNetworkBuffer->pucEthernetBuffer );
+    }
+}
+
 BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDescriptor,
                                                 NetworkBufferDescriptor_t * const pxNetworkBuffer,
                                                 BaseType_t xReleaseAfterSend )
@@ -81,6 +98,14 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes
     __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "The ethernet buffer cannot be NULL." );
 }
 
+BaseType_t xIsCallingFromIPTask( void )
+{
+    BaseType_t xReturn;
+
+    __CPROVER_assume( xReturn == pdFALSE || xReturn == pdTRUE );
+
+    return xReturn;
+}
 
 void harness()
 {
@@ -92,16 +117,16 @@ void harness()
      * Assumes one endpoint and interface is present.
      */
 
-    pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    pxNetworkEndPoints = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
     __CPROVER_assume( pxNetworkEndPoints != NULL );
 
     /* Interface init. */
-    pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
+    pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) );
     __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
 
     if( nondet_bool() )
     {
-        pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+        pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
         __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
         pxNetworkEndPoints->pxNext->pxNext = NULL;
         pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;

From 4c4426f980cc9aa50778117a59c5ef3e4a135808 Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Tue, 9 Jul 2024 07:27:40 +0000
Subject: [PATCH 06/36] Fix ARP_OutputARPRequest_buffer_alloc1 CBMC test

---
 .../Configurations.json                                   | 4 +++-
 .../OutputARPRequest_harness.c                            | 8 ++++++++
 2 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json
index e243382c3..110247a03 100644
--- a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json
+++ b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json
@@ -14,7 +14,9 @@
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
     "$(FREERTOS_PLUS_TCP)/source/portable/BufferManagement/BufferAllocation_1.goto",
     "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto",
-    "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/queue.goto"
+    "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/queue.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/proofs/CBMCStubLibrary/tasksStubs.c",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto"
   ],
   "DEF":
   [
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
index 492d97683..03c74e467 100644
--- a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c
+++ b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/OutputARPRequest_harness.c
@@ -75,6 +75,14 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes
     }
 }
 
+BaseType_t xIsCallingFromIPTask( void )
+{
+    BaseType_t xReturn;
+
+    __CPROVER_assume( xReturn == pdFALSE || xReturn == pdTRUE );
+
+    return xReturn;
+}
 
 void harness()
 {

From 1bb5934e82aaf11f1d36622054184c749a3fed93 Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Tue, 9 Jul 2024 09:19:46 +0000
Subject: [PATCH 07/36] Fix ARP_OutputARPRequest_buffer_alloc2 CBMC test

---
 .../Configurations.json                                  | 4 +++-
 .../OutputARPRequest_harness.c                           | 9 +++++++++
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json
index 5b2cdd30d..d37f17720 100644
--- a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json
+++ b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json
@@ -14,7 +14,9 @@
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
     "$(FREERTOS_PLUS_TCP)/source/portable/BufferManagement/BufferAllocation_2.goto",
     "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto",
-    "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/queue.goto"
+    "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/queue.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/proofs/CBMCStubLibrary/tasksStubs.goto"
   ],
   "DEF":
   [
diff --git a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c
index 4d8493449..b87ae8b30 100644
--- a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c
+++ b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/OutputARPRequest_harness.c
@@ -55,6 +55,15 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes
     }
 }
 
+BaseType_t xIsCallingFromIPTask( void )
+{
+    BaseType_t xReturn;
+
+    __CPROVER_assume( xReturn == pdFALSE || xReturn == pdTRUE );
+
+    return xReturn;
+}
+
 void harness()
 {
     BaseType_t xRes = xNetworkBuffersInitialise();

From 9eb18c8f9c283e114a4c790e9c17ad24cafbed79 Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Tue, 9 Jul 2024 10:08:06 +0000
Subject: [PATCH 08/36] Fix CheckOptionsInner CBMC test

---
 .../cbmc/proofs/CheckOptionsInner/CheckOptionsInner_harness.c | 2 +-
 test/cbmc/proofs/CheckOptionsInner/Makefile.json              | 4 +++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/test/cbmc/proofs/CheckOptionsInner/CheckOptionsInner_harness.c b/test/cbmc/proofs/CheckOptionsInner/CheckOptionsInner_harness.c
index e4a08e2ee..8ac5d6a82 100644
--- a/test/cbmc/proofs/CheckOptionsInner/CheckOptionsInner_harness.c
+++ b/test/cbmc/proofs/CheckOptionsInner/CheckOptionsInner_harness.c
@@ -87,7 +87,7 @@ void harness()
     /* Preconditions */
 
     /* CBMC model of pointers limits the size of the buffer */
-    __CPROVER_assume( buffer_size < CBMC_MAX_OBJECT_SIZE );
+    __CPROVER_assume( buffer_size < ipconfigNETWORK_MTU );
 
     /* Both preconditions are required to avoid integer overflow in the */
     /* pointer offset of the pointer pucPtr + uxIndex + 8 */
diff --git a/test/cbmc/proofs/CheckOptionsInner/Makefile.json b/test/cbmc/proofs/CheckOptionsInner/Makefile.json
index a902bcc94..522ca4cca 100644
--- a/test/cbmc/proofs/CheckOptionsInner/Makefile.json
+++ b/test/cbmc/proofs/CheckOptionsInner/Makefile.json
@@ -12,6 +12,7 @@
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Reception.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_IP.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_WIN.goto",
@@ -21,6 +22,7 @@
   ],
   "DEF":
   [
-    "ipconfigUSE_TCP=1"
+    "ipconfigUSE_TCP=1",
+    "ipconfigNETWORK_MTU=586"
   ]
 }

From 85a41690dc7a5ef8bfd919ffe1147588374ff955 Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Tue, 9 Jul 2024 10:09:54 +0000
Subject: [PATCH 09/36] Fix CheckOptionsOuter CBMC test

---
 test/cbmc/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c | 2 +-
 test/cbmc/proofs/CheckOptionsOuter/Makefile.json               | 2 ++
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/test/cbmc/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c b/test/cbmc/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c
index 3d58d0dd1..867305d93 100644
--- a/test/cbmc/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c
+++ b/test/cbmc/proofs/CheckOptionsOuter/CheckOptionsOuter_harness.c
@@ -81,7 +81,7 @@ void harness()
     ****************************************************************/
 
     /* CBMC model of pointers limits the size of the buffer */
-    __CPROVER_assume( buffer_size < CBMC_MAX_OBJECT_SIZE );
+    __CPROVER_assume( buffer_size < ipconfigNETWORK_MTU );
 
     /* Preconditions */
     __CPROVER_assume( 8 <= buffer_size ); /* ulFirst and ulLast */
diff --git a/test/cbmc/proofs/CheckOptionsOuter/Makefile.json b/test/cbmc/proofs/CheckOptionsOuter/Makefile.json
index d97be23e6..898d1ea5b 100644
--- a/test/cbmc/proofs/CheckOptionsOuter/Makefile.json
+++ b/test/cbmc/proofs/CheckOptionsOuter/Makefile.json
@@ -12,6 +12,7 @@
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Reception.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_WIN.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Stream_Buffer.goto",
@@ -20,5 +21,6 @@
   ],
   "DEF":
   [
+    "ipconfigNETWORK_MTU=586"
   ]
 }

From 78a313d8fd7086bda7fa1f999e529dc1b0f552c4 Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Tue, 9 Jul 2024 10:21:31 +0000
Subject: [PATCH 10/36] Fix DHCPProcess CBMC test

---
 test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c | 7 +++++++
 test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json         | 3 ++-
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c
index 10c6aacf8..29fabf657 100644
--- a/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c
+++ b/test/cbmc/proofs/DHCP/DHCPProcess/DHCPProcess_harness.c
@@ -166,6 +166,13 @@ int32_t FreeRTOS_recvfrom( Socket_t xSocket,
     return retVal;
 }
 
+void * vSocketClose( FreeRTOS_Socket_t * pxSocket )
+{
+    __CPROVER_assert( pxSocket != NULL, "Closing socket cannot be NULL." );
+
+    return NULL;
+}
+
 /****************************************************************
 * The proof of vDHCPProcess
 ****************************************************************/
diff --git a/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json b/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json
index 99e79d3b2..f74a67537 100644
--- a/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json
+++ b/test/cbmc/proofs/DHCP/DHCPProcess/Makefile.json
@@ -24,7 +24,8 @@
     "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCP.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto"
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto"
   ],
   "DEF":
   [

From 408d58a241a9139dc8411e4fd7f37832a54b6fae Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Wed, 10 Jul 2024 02:57:13 +0000
Subject: [PATCH 11/36] Fix DHCPProcessEndPoint CBMC test

---
 .../DHCPProcessEndPoint_harness.c             | 30 +++++++++++++++++++
 .../DHCP/DHCPProcessEndPoint/Makefile.json    |  2 ++
 test/cbmc/stubs/freertos_api.c                | 17 +++++++++++
 3 files changed, 49 insertions(+)

diff --git a/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/DHCPProcessEndPoint_harness.c b/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/DHCPProcessEndPoint_harness.c
index db482595c..bd53b2745 100644
--- a/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/DHCPProcessEndPoint_harness.c
+++ b/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/DHCPProcessEndPoint_harness.c
@@ -145,6 +145,35 @@ Socket_t FreeRTOS_socket( BaseType_t xDomain,
     return ensure_FreeRTOS_Socket_t_is_allocated();
 }
 
+void vApplicationIPNetworkEventHook_Multi( eIPCallbackEvent_t eNetworkEvent,
+                                           struct xNetworkEndPoint * pxEndPoint )
+{
+    __CPROVER_assert( eNetworkEvent == eNetworkUp || eNetworkEvent == eNetworkDown, "Network event is not correct" );
+    __CPROVER_assert( pxEndPoint != NULL, "Endpoint cannot be NULL" );
+}
+
+BaseType_t xIsCallingFromIPTask( void )
+{
+    BaseType_t xReturn;
+
+    __CPROVER_assume( xReturn == pdFALSE || xReturn == pdTRUE );
+
+    return xReturn;
+}
+
+void * vSocketClose( FreeRTOS_Socket_t * pxSocket )
+{
+    __CPROVER_assert( pxSocket != NULL, "Closing socket cannot be NULL" );
+
+    return NULL;
+}
+
+void vManageSolicitedNodeAddress( const struct xNetworkEndPoint * pxEndPoint,
+                                  BaseType_t xNetworkGoingUp )
+{
+    __CPROVER_assert( pxEndPoint != NULL, "Endpoint cannot be NULL" );
+    __CPROVER_assert( pxEndPoint->pxNetworkInterface != NULL, "The network interface cannot be NULL" );
+}
 
 /****************************************************************
 * The proof of vDHCPProcess
@@ -178,6 +207,7 @@ void harness()
     __CPROVER_assume( pxNetworkEndPoint_Temp != NULL );
     pxNetworkEndPoint_Temp->pxNext = NULL;
     pxNetworkEndPoint_Temp->xDHCPData.xDHCPSocket = NULL;
+    pxNetworkEndPoint_Temp->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
 
     /****************************************************************
     * Initialize the counter used to bound the number of times
diff --git a/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/Makefile.json b/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/Makefile.json
index ed7497613..59cfc8cc6 100644
--- a/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/Makefile.json
+++ b/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/Makefile.json
@@ -23,8 +23,10 @@
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
     "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCP.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto"
   ],
   "DEF":
diff --git a/test/cbmc/stubs/freertos_api.c b/test/cbmc/stubs/freertos_api.c
index cc13622c6..3edadc623 100644
--- a/test/cbmc/stubs/freertos_api.c
+++ b/test/cbmc/stubs/freertos_api.c
@@ -398,3 +398,20 @@ void vIPSetARPResolutionTimerEnableState( BaseType_t xEnableState )
 }
 
 /****************************************************************/
+
+/****************************************************************
+* Abstract vIPSetARPResolutionTimerEnableState
+****************************************************************/
+BaseType_t xApplicationGetRandomNumber( uint32_t * pulNumber )
+{
+    __CPROVER_assert( pulNumber != NULL, "The input number cannot be NULL" );
+
+    BaseType_t xReturn;
+
+    *pulNumber = nondet_uint32();
+
+    /* Return some random value. */
+    return xReturn;
+}
+
+/****************************************************************/

From da1b4a986e2b7fff8928edbbda1930792e8bcf8b Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Wed, 10 Jul 2024 03:05:46 +0000
Subject: [PATCH 12/36] Fix DHCPv6HandleOption CBMC test

---
 .../DHCPv6HandleOption_harness.c                | 17 +++++++++++++++++
 .../DHCPv6/DHCPv6HandleOption/Makefile.json     |  6 ------
 2 files changed, 17 insertions(+), 6 deletions(-)

diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/DHCPv6HandleOption_harness.c b/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/DHCPv6HandleOption_harness.c
index 7a5495313..5800b6082 100644
--- a/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/DHCPv6HandleOption_harness.c
+++ b/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/DHCPv6HandleOption_harness.c
@@ -74,6 +74,23 @@ BaseType_t __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6_subOption( uint16_t
     return nondet_BaseType();
 }
 
+uint16_t usBitConfig_read_16( BitConfig_t * pxConfig )
+{
+    return (uint16_t) nondet_uint32();
+}
+
+uint8_t ucBitConfig_read_8( BitConfig_t * pxConfig )
+{
+    return (uint8_t) nondet_uint32();
+}
+
+BaseType_t xBitConfig_read_uc( BitConfig_t * pxConfig,
+                               uint8_t * pucData,
+                               size_t uxSize )
+{
+    return nondet_BaseType();
+}
+
 void harness()
 {
     BaseType_t xResult;
diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/Makefile.json
index 09859a60b..ba6dbd18f 100644
--- a/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/Makefile.json
+++ b/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/Makefile.json
@@ -5,12 +5,6 @@
       "--unwind 2",
       "--nondet-static --flush"
     ],
-    "INSTFLAGS":
-    [
-        "--remove-function-body usBitConfig_read_16",
-        "--remove-function-body xBitConfig_read_uc",
-        "--remove-function-body ucBitConfig_read_8"
-    ],
     "OPT":
     [
       "--export-file-local-symbols"

From 115db5add3216f83bfb8c3267663bbd1e9f74459 Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Wed, 10 Jul 2024 03:09:53 +0000
Subject: [PATCH 13/36] Fix DHCPv6Process CBMC test

---
 test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json
index 40839470b..fba06214b 100644
--- a/test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json
+++ b/test/cbmc/proofs/DHCPv6/DHCPv6Process/Makefile.json
@@ -19,6 +19,9 @@
     [
       "$(ENTRY)_harness.goto",
       "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
-      "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCPv6.goto"
+      "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
+      "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto",
+      "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCPv6.goto",
+      "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto"
     ]
 }
\ No newline at end of file

From 5ac70269cba306bb6da02ffc3a5214ff386bec59 Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Wed, 10 Jul 2024 03:14:18 +0000
Subject: [PATCH 14/36] Fix DHCPv6ProcessEndPoint CBMC test

---
 .../DHCPv6ProcessEndPoint_harness.c                  | 12 ++++++++++++
 .../DHCPv6/DHCPv6ProcessEndPoint/Makefile.json       | 10 ++--------
 2 files changed, 14 insertions(+), 8 deletions(-)

diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/DHCPv6ProcessEndPoint_harness.c b/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/DHCPv6ProcessEndPoint_harness.c
index 9157a86f2..350c13cce 100644
--- a/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/DHCPv6ProcessEndPoint_harness.c
+++ b/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/DHCPv6ProcessEndPoint_harness.c
@@ -77,6 +77,18 @@ Socket_t FreeRTOS_socket( BaseType_t xDomain,
     return pxSocket;
 }
 
+void vIPNetworkUpCalls( struct xNetworkEndPoint * pxEndPoint )
+{
+    __CPROVER_assert( pxEndPoint != NULL, "Endpoint cannot be NULL" );
+}
+
+void * vSocketClose( FreeRTOS_Socket_t * pxSocket )
+{
+    __CPROVER_assert( pxSocket != NULL, "Closing socket cannot be NULL." );
+
+    return NULL;
+}
+
 /**
  * For the purpose of this proof we assume that xSocketValid returns true always.
  * This has to do with assertions in the source code that checks for socket being invalid.
diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/Makefile.json b/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/Makefile.json
index d2d5931bc..21e1105ac 100644
--- a/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/Makefile.json
+++ b/test/cbmc/proofs/DHCPv6/DHCPv6ProcessEndPoint/Makefile.json
@@ -5,14 +5,6 @@
       "--nondet-static --flush",
       "--unwind 1"
     ],
-    "INSTFLAGS":
-    [
-        "--remove-function-body vIPSetDHCP_RATimerEnableState",
-        "--remove-function-body vDHCP_RATimerReload",
-        "--remove-function-body vIPNetworkUpCalls",
-        "--remove-function-body prvCloseDHCPv6Socket",
-        "--remove-function-body prvSendDHCPMessage"
-    ],
     "OPT":
     [
       "--export-file-local-symbols"
@@ -25,6 +17,8 @@
     [
       "$(ENTRY)_harness.goto",
       "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
+      "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
+      "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto",
       "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCPv6.goto",
       "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
       "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto"

From 598d87a563862777176f035bb497661901ef6fe9 Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Wed, 10 Jul 2024 03:46:33 +0000
Subject: [PATCH 15/36] Fix SendDHCPMessage CBMC test

---
 .../DHCPv6/SendDHCPMessage/Makefile.json      | 20 +---
 .../SendDHCPMessage/SendDHCPMessage_harness.c | 91 ++++++++++++++++++-
 2 files changed, 93 insertions(+), 18 deletions(-)

diff --git a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/Makefile.json b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/Makefile.json
index 08cb3e73a..98bc9f724 100644
--- a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/Makefile.json
+++ b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/Makefile.json
@@ -4,20 +4,6 @@
     [
       "--nondet-static"
     ],
-    "INSTFLAGS":
-    [
-      "--remove-function-body xApplicationGetRandomNumber",
-      "--remove-function-body ulApplicationTimeHook",
-      "--remove-function-body xBitConfig_init",
-      "--remove-function-body vBitConfig_write_8",
-      "--remove-function-body vBitConfig_write_uc",
-      "--remove-function-body vBitConfig_write_16",
-      "--remove-function-body vBitConfig_write_32",
-      "--remove-function-body pucBitConfig_peek_last_index_uc",
-      "--remove-function-body FreeRTOS_inet_pton6",
-      "--remove-function-body FreeRTOS_sendto",
-      "--remove-function-body vBitConfig_release"
-    ],
     "OPT":
     [
       "--export-file-local-symbols"
@@ -29,9 +15,9 @@
     "OBJS":
     [
       "$(ENTRY)_harness.goto",
+      "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCPv6.goto",
       "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
-      "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Sockets.goto",
-      "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_BitConfig.goto",
-      "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DHCPv6.goto"
+      "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
+      "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto"
     ]
 }
\ No newline at end of file
diff --git a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c
index fc2886720..436b96cf5 100644
--- a/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c
+++ b/test/cbmc/proofs/DHCPv6/SendDHCPMessage/SendDHCPMessage_harness.c
@@ -42,14 +42,103 @@
 #include "FreeRTOS_DHCP.h"
 #include "FreeRTOS_DHCPv6.h"
 #include "FreeRTOS_ARP.h"
+#include "FreeRTOS_BitConfig.h"
 
 /* CBMC includes. */
 #include "cbmc.h"
 
+void __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvSendDHCPMessage( NetworkEndPoint_t * pxEndPoint );
 
+BaseType_t xBitConfig_init( BitConfig_t * pxConfig,
+                            const uint8_t * pucData,
+                            size_t uxSize )
+{
+    BaseType_t xReturn;
 
-void __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvSendDHCPMessage( NetworkEndPoint_t * pxEndPoint );
+    __CPROVER_assert( pxConfig != NULL, "pxConfig cannot be NULL" );
+
+    if( nondet_bool() )
+    {
+        xReturn = pdTRUE;
+
+        pxConfig->ucContents = safeMalloc( uxSize );
+        __CPROVER_assume( pxConfig->ucContents != NULL );
+    }
+    else
+    {
+        xReturn = pdFALSE;
+    }
+
+    return xReturn;
+}
+
+BaseType_t pucBitConfig_peek_last_index_uc( BitConfig_t * pxConfig,
+                                            uint8_t * pucData,
+                                            size_t uxSize )
+{
+    BaseType_t xReturn;
+
+    __CPROVER_assert( pxConfig != NULL, "pxConfig cannot be NULL" );
+    __CPROVER_assert( pucData != NULL, "pucData cannot be NULL" );
+
+    __CPROVER_assume( xReturn == pdTRUE || xReturn == pdFALSE );
+
+    return xReturn;
+}
+
+void vBitConfig_write_uc( BitConfig_t * pxConfig,
+                          const uint8_t * pucData,
+                          size_t uxSize )
+{
+    __CPROVER_assert( pxConfig != NULL, "pxConfig cannot be NULL" );
+    __CPROVER_assert( pucData != NULL, "pucData cannot be NULL" );
+}
+
+void vBitConfig_write_8( BitConfig_t * pxConfig,
+                         uint8_t ucValue )
+{
+    __CPROVER_assert( pxConfig != NULL, "pxConfig cannot be NULL" );
+}
 
+void vBitConfig_write_16( BitConfig_t * pxConfig,
+                          uint16_t usValue )
+{
+    __CPROVER_assert( pxConfig != NULL, "pxConfig cannot be NULL" );
+}
+
+void vBitConfig_write_32( BitConfig_t * pxConfig,
+                          uint32_t ulValue )
+{
+    __CPROVER_assert( pxConfig != NULL, "pxConfig cannot be NULL" );
+}
+
+void vBitConfig_release( BitConfig_t * pxConfig )
+{
+    __CPROVER_assert( pxConfig != NULL, "pxConfig cannot be NULL" );
+
+    if( pxConfig->ucContents != NULL )
+    {
+        free( pxConfig->ucContents );
+    }
+}
+
+BaseType_t FreeRTOS_inet_pton6( const char * pcSource,
+                                void * pvDestination )
+{
+    BaseType_t xReturn;
+
+    __CPROVER_assert( pcSource != NULL, "pcSource cannot be NULL" );
+    __CPROVER_assert( pvDestination != NULL, "pvDestination cannot be NULL" );
+
+    __CPROVER_assume( xReturn == pdTRUE || xReturn == pdFALSE );
+
+    return xReturn;
+}
+
+uint32_t ulApplicationTimeHook( void )
+{
+    return nondet_uint32();
+}
 
 void harness()
 {

From 6a7eff080e210df732d1a37ba2f753e67dd1ff0b Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Thu, 11 Jul 2024 02:54:30 +0000
Subject: [PATCH 16/36] Fix DNSHandlePacket CBMC test

---
 .../DNS/DNSHandlePacket/DNShandlePacket_harness.c | 15 +++++++++++----
 .../cbmc/proofs/DNS/DNSHandlePacket/Makefile.json |  3 ++-
 2 files changed, 13 insertions(+), 5 deletions(-)

diff --git a/test/cbmc/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c b/test/cbmc/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c
index 983f1f109..52106ba65 100644
--- a/test/cbmc/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c
+++ b/test/cbmc/proofs/DNS/DNSHandlePacket/DNShandlePacket_harness.c
@@ -7,11 +7,18 @@
 #include "FreeRTOS_DNS.h"
 #include "FreeRTOS_IP_Private.h"
 
-/* Function prvParseDNSReply is proven to be correct separately. */
-uint32_t prvParseDNSReply( uint8_t * pucUDPPayloadBuffer,
-                           size_t xBufferLength,
-                           BaseType_t xExpected )
+/* CBMC includes. */
+#include "cbmc.h"
+
+/* Function DNS_ParseDNSReply is proven to be correct separately. */
+uint32_t DNS_ParseDNSReply( uint8_t * pucUDPPayloadBuffer,
+                            size_t uxBufferLength,
+                            struct freertos_addrinfo ** ppxAddressInfo,
+                            BaseType_t xExpected,
+                            uint16_t usPort )
 {
+    __CPROVER_assert( pucUDPPayloadBuffer != NULL, "pucUDPPayloadBuffer cannot be NULL" );
+    return nondet_uint32();
 }
 
 void harness()
diff --git a/test/cbmc/proofs/DNS/DNSHandlePacket/Makefile.json b/test/cbmc/proofs/DNS/DNSHandlePacket/Makefile.json
index 27864b146..511a166ca 100644
--- a/test/cbmc/proofs/DNS/DNSHandlePacket/Makefile.json
+++ b/test/cbmc/proofs/DNS/DNSHandlePacket/Makefile.json
@@ -4,7 +4,8 @@
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto"
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto"
   ],
   "DEF":
   [

From 3b682218f51a6f4238f65ce1bcf408100322487c Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Thu, 11 Jul 2024 03:19:16 +0000
Subject: [PATCH 17/36] Fix ARP CBMC test

---
 .../ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json  | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json
index 110247a03..ff5898c18 100644
--- a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json
+++ b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json
@@ -15,7 +15,7 @@
     "$(FREERTOS_PLUS_TCP)/source/portable/BufferManagement/BufferAllocation_1.goto",
     "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto",
     "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/queue.goto",
-    "$(FREERTOS_PLUS_TCP)/test/cbmc/proofs/CBMCStubLibrary/tasksStubs.c",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/proofs/CBMCStubLibrary/tasksStubs.goto",
     "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto"
   ],
   "DEF":

From bbb78b29517646de9f33c5d787722c1fa5902e31 Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Thu, 11 Jul 2024 05:54:34 +0000
Subject: [PATCH 18/36] Fix DNSTreatNBNS CBMC test

---
 source/FreeRTOS_DNS_Cache.c                   |  3 +--
 .../DNS/DNSTreatNBNS/DNS_TreatNBNS_harness.c  | 27 +++++++++++++++++++
 .../proofs/DNS/DNSTreatNBNS/Makefile.json     | 14 +++++++---
 3 files changed, 38 insertions(+), 6 deletions(-)

diff --git a/source/FreeRTOS_DNS_Cache.c b/source/FreeRTOS_DNS_Cache.c
index 7c8e23638..119be881d 100644
--- a/source/FreeRTOS_DNS_Cache.c
+++ b/source/FreeRTOS_DNS_Cache.c
@@ -448,10 +448,9 @@
         /* Add or update the item. */
         if( strlen( pcName ) < ( size_t ) ipconfigDNS_CACHE_NAME_LENGTH )
         {
-            ( void ) strncpy( xDNSCache[ uxFreeEntry ].pcName, pcName, ipconfigDNS_CACHE_NAME_LENGTH );
+            ( void ) strncpy( xDNSCache[ uxFreeEntry ].pcName, pcName, strlen( pcName ) );
             ( void ) memcpy( &( xDNSCache[ uxFreeEntry ].xAddresses[ 0 ] ), pxIP, sizeof( *pxIP ) );
 
-
             xDNSCache[ uxFreeEntry ].ulTTL = ulTTL;
             xDNSCache[ uxFreeEntry ].ulTimeWhenAddedInSeconds = ulCurrentTimeSeconds;
             #if ( ipconfigDNS_CACHE_ADDRESSES_PER_ENTRY > 1 )
diff --git a/test/cbmc/proofs/DNS/DNSTreatNBNS/DNS_TreatNBNS_harness.c b/test/cbmc/proofs/DNS/DNSTreatNBNS/DNS_TreatNBNS_harness.c
index d6be53942..7d1d70669 100644
--- a/test/cbmc/proofs/DNS/DNSTreatNBNS/DNS_TreatNBNS_harness.c
+++ b/test/cbmc/proofs/DNS/DNSTreatNBNS/DNS_TreatNBNS_harness.c
@@ -38,6 +38,7 @@
 
 #include "cbmc.h"
 
+const BaseType_t xBufferAllocFixedSize = pdFALSE;
 NetworkBufferDescriptor_t xNetworkBuffer;
 
 NetworkBufferDescriptor_t * pxUDPPayloadBuffer_to_NetworkBuffer( const void * pvBuffer )
@@ -67,6 +68,11 @@ NetworkBufferDescriptor_t * pxResizeNetworkBufferWithDescriptor( NetworkBufferDe
     uint8_t * pucNewBuffer = safeMalloc( xNewSizeBytes );
     __CPROVER_assume( pucNewBuffer != NULL );
 
+    if( pxNetworkBuffer->pucEthernetBuffer )
+    {
+        free( pxNetworkBuffer->pucEthernetBuffer );
+    }
+
     pxNetworkBuffer->pucEthernetBuffer = pucNewBuffer;
 
     if( nondet_bool() )
@@ -88,6 +94,26 @@ void prepareReplyDNSMessage( NetworkBufferDescriptor_t * pxNetworkBuffer,
     __CPROVER_assert( pxNetworkBuffer != NULL, "pxNetworkBuffer: pvBuffer != NULL" );
 }
 
+BaseType_t xApplicationDNSQueryHook_Multi( struct xNetworkEndPoint * pxEndPoint,
+                                           const char * pcName )
+{
+    BaseType_t xReturn;
+
+    __CPROVER_assert( strlen( pcName ) < ipconfigDNS_CACHE_NAME_LENGTH, "The length of domain name must be less than cache size" );
+    __CPROVER_assume( xReturn == pdFALSE || xReturn == pdTRUE );
+
+    return xReturn;
+}
+
+/* vReturnEthernetFrame() is proved separately */
+void vReturnEthernetFrame( NetworkBufferDescriptor_t * pxNetworkBuffer,
+                           BaseType_t xReleaseAfterSend )
+{
+    __CPROVER_assert( pxNetworkBuffer != NULL, "xNetworkBuffer != NULL" );
+    __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "pxNetworkBuffer->pucEthernetBuffer != NULL" );
+    __CPROVER_assert( __CPROVER_r_ok( pxNetworkBuffer->pucEthernetBuffer, pxNetworkBuffer->xDataLength ), "Data must be valid" );
+}
+
 void harness()
 {
     uint32_t ulIPAddress;
@@ -103,6 +129,7 @@ void harness()
 
     xNetworkBuffer.pucEthernetBuffer = safeMalloc( xDataSize );
     xNetworkBuffer.xDataLength = xDataSize;
+    __CPROVER_assume( xNetworkBuffer.pucEthernetBuffer != NULL );
 
     if( nondet_bool() )
     {
diff --git a/test/cbmc/proofs/DNS/DNSTreatNBNS/Makefile.json b/test/cbmc/proofs/DNS/DNSTreatNBNS/Makefile.json
index 458443eb7..d3ab0d582 100644
--- a/test/cbmc/proofs/DNS/DNSTreatNBNS/Makefile.json
+++ b/test/cbmc/proofs/DNS/DNSTreatNBNS/Makefile.json
@@ -1,18 +1,24 @@
 {
   "ENTRY": "DNS_TreatNBNS",
   "USE_CACHE":1,
+  "NBNS_NAME_MAX_LENGTH":17,
   "CBMCFLAGS":
   [
   	"--unwind 1",
-    "--unwindset DNS_TreatNBNS.0:16",
-  	"--nondet-static"
+    "--unwindset DNS_TreatNBNS.0:{NBNS_NAME_MAX_LENGTH}",
+    "--unwindset prvFindEntryIndex.0:2",
+    "--unwindset strcmp.0:{NBNS_NAME_MAX_LENGTH}",
+    "--unwindset strlen.0:{NBNS_NAME_MAX_LENGTH}",
+    "--unwindset strncpy.0:{NBNS_NAME_MAX_LENGTH}"
   ],
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
-    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto"
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Cache.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto"
   ],
   "DEF":
   [

From 0c2b88c3b15580d165125de20dd30a858e99ce35 Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Thu, 11 Jul 2024 07:37:22 +0000
Subject: [PATCH 19/36] Fix DNSgetHostByName and DNSgetHostByName_a CBMC test

---
 source/FreeRTOS_IP.c                          |   6 +-
 source/FreeRTOS_IP_Utils.c                    |  34 +++---
 .../DNSgetHostByName_harness.c                |  49 +++++++-
 .../proofs/DNS/DNSgetHostByName/Makefile.json |  10 +-
 .../DNSgetHostByName_a_harness.c              | 111 +++++++++++++++++-
 .../DNS/DNSgetHostByName_a/Makefile.json      |   6 +-
 6 files changed, 187 insertions(+), 29 deletions(-)

diff --git a/source/FreeRTOS_IP.c b/source/FreeRTOS_IP.c
index 3765e85a4..54b3e0d39 100644
--- a/source/FreeRTOS_IP.c
+++ b/source/FreeRTOS_IP.c
@@ -1042,8 +1042,10 @@ void FreeRTOS_ReleaseUDPPayloadBuffer( void const * pvBuffer )
     NetworkBufferDescriptor_t * pxBuffer;
 
     pxBuffer = pxUDPPayloadBuffer_to_NetworkBuffer( pvBuffer );
-    configASSERT( pxBuffer != NULL );
-    vReleaseNetworkBufferAndDescriptor( pxBuffer );
+    if( pxBuffer != NULL )
+    {
+        vReleaseNetworkBufferAndDescriptor( pxBuffer );
+    }
 }
 /*-----------------------------------------------------------*/
 
diff --git a/source/FreeRTOS_IP_Utils.c b/source/FreeRTOS_IP_Utils.c
index 3c27eb8bc..c9e64b857 100644
--- a/source/FreeRTOS_IP_Utils.c
+++ b/source/FreeRTOS_IP_Utils.c
@@ -747,32 +747,32 @@ NetworkBufferDescriptor_t * pxUDPPayloadBuffer_to_NetworkBuffer( const void * pv
          * for a IPv6 packet, pucIPType will point to the first byte of the IP-header: 'ucVersionTrafficClass'. */
         ucIPType = pucIPType[ 0 ] & 0xf0U;
 
-        /* To help the translation from a UDP payload pointer to a networkBuffer,
-         * a byte was stored at a certain negative offset (-48 bytes).
-         * It must have a value of either 0x4x or 0x6x. */
-        configASSERT( ( ucIPType == ipTYPE_IPv4 ) || ( ucIPType == ipTYPE_IPv6 ) );
-
         switch( ucIPType ) /* LCOV_EXCL_BR_LINE */
         {
-            #if ( ipconfigUSE_IPv6 != 0 )
-                case ipTYPE_IPv6:
-                    uxOffset = sizeof( UDPPacket_IPv6_t );
-                    break;
-            #endif /* ( ipconfigUSE_IPv6 != 0 ) */
+            /* For Rx path, it's possible to receive packets that is disabled. We should be able to get the network
+             * descriptor to free that network buffer correctly. */
+            case ipTYPE_IPv6:
+                uxOffset = sizeof( UDPPacket_IPv6_t );
+                break;
 
-            #if ( ipconfigUSE_IPv4 != 0 )
-                case ipTYPE_IPv4:
-                    uxOffset = sizeof( UDPPacket_t );
-                    break;
-            #endif /* ( ipconfigUSE_IPv4 != 0 ) */
+            case ipTYPE_IPv4:
+                uxOffset = sizeof( UDPPacket_t );
+                break;
 
             default:
                 FreeRTOS_debug_printf( ( "pxUDPPayloadBuffer_to_NetworkBuffer: Undefined ucIPType \n" ) );
-                uxOffset = sizeof( UDPPacket_t );
+                uxOffset = 0;
                 break;
         }
 
-        pxResult = prvPacketBuffer_to_NetworkBuffer( pvBuffer, uxOffset );
+        if( uxOffset != 0 )
+        {
+            pxResult = prvPacketBuffer_to_NetworkBuffer( pvBuffer, uxOffset );
+        }
+        else
+        {
+            pxResult = NULL;
+        }
     }
 
     return pxResult;
diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c
index e849b4ee1..71b53cee8 100644
--- a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c
+++ b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c
@@ -96,6 +96,22 @@ uint32_t DNS_SendRequest( Socket_t xDNSSocket,
     return ret;
 }
 
+/****************************************************************
+* Abstract  DNS_BindSocket
+*
+* We stub out this function with return constraint of true or false
+*
+****************************************************************/
+BaseType_t DNS_BindSocket( Socket_t xSocket,
+                           uint16_t usPort )
+{
+    BaseType_t xReturn;
+
+    __CPROVER_assume( xReturn == pdTRUE || xReturn == pdFALSE );
+
+    return xReturn;
+}
+
 /****************************************************************
 * Abstract DNS_ReadReply
 *
@@ -182,11 +198,11 @@ size_t __CPROVER_file_local_FreeRTOS_DNS_c_prvCreateDNSMessage( uint8_t * pucUDP
 NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes,
                                                               TickType_t xBlockTimeTicks )
 {
-    NetworkBufferDescriptor_t * pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) malloc( sizeof( NetworkBufferDescriptor_t ) );
+    NetworkBufferDescriptor_t * pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
 
     if( pxNetworkBuffer != NULL )
     {
-        pxNetworkBuffer->pucEthernetBuffer = malloc( xRequestedSizeBytes + ipUDP_PAYLOAD_IP_TYPE_OFFSET );
+        pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xRequestedSizeBytes + ipUDP_PAYLOAD_IP_TYPE_OFFSET );
 
         if( pxNetworkBuffer->pucEthernetBuffer == NULL )
         {
@@ -203,6 +219,35 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS
     return pxNetworkBuffer;
 }
 
+/*
+ * In this function, it only allocates network buffer by pxGetNetworkBufferWithDescriptor
+ * stub function above here. In this case, we should free both network buffer descriptor and pucEthernetBuffer.
+ */
+void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer )
+{
+    __CPROVER_assert( pxNetworkBuffer != NULL,
+                      "Precondition: pxNetworkBuffer != NULL" );
+
+    free( pxNetworkBuffer->pucEthernetBuffer - ipUDP_PAYLOAD_IP_TYPE_OFFSET );
+    free( pxNetworkBuffer );
+}
+
+/* FreeRTOS_ReleaseUDPPayloadBuffer is mocked here and the memory
+ * is not freed as the buffer allocated by the FreeRTOS_recvfrom is static
+ * memory */
+void FreeRTOS_ReleaseUDPPayloadBuffer( void * pvBuffer )
+{
+    __CPROVER_assert( pvBuffer != NULL,
+                      "FreeRTOS precondition: pvBuffer != NULL" );
+}
+
+uint32_t Prepare_CacheLookup( const char * pcHostName,
+                              BaseType_t xFamily,
+                              struct freertos_addrinfo ** ppxAddressInfo )
+{
+    return nondet_uint32();
+}
+
 /****************************************************************
 * The proof for FreeRTOS_gethostbyname.
 ****************************************************************/
diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json
index 66b7cad54..6df4759db 100644
--- a/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json
+++ b/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json
@@ -11,6 +11,7 @@
   "ENDPOINT_DNS_ADDRESS_COUNT": 5,
   "HOSTNAME_UNWIND": "__eval {MAX_HOSTNAME_LEN} + 1",
   "ENDPOINT_DNS_ADDRESS_COUNT_UNWIND": "__eval {ENDPOINT_DNS_ADDRESS_COUNT} + 1",
+  "DNS_CACHE_ENTRIES": 2,
 
   "CBMCFLAGS":
   [
@@ -30,11 +31,13 @@
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
-    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto"
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto"
   ],
 
   "DEF":
@@ -42,6 +45,7 @@
     "ipconfigUSE_IPv6=1",
     "ipconfigDNS_USE_CALLBACKS={callback}",
     "MAX_HOSTNAME_LEN={MAX_HOSTNAME_LEN}",
-    "ipconfigENDPOINT_DNS_ADDRESS_COUNT={ENDPOINT_DNS_ADDRESS_COUNT}"
+    "ipconfigENDPOINT_DNS_ADDRESS_COUNT={ENDPOINT_DNS_ADDRESS_COUNT}",
+    "ipconfigDNS_CACHE_ENTRIES={DNS_CACHE_ENTRIES}"
   ]
 }
diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c
index 7b7c4a3fb..bcef7792b 100644
--- a/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c
+++ b/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c
@@ -116,11 +116,11 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes
 NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes,
                                                               TickType_t xBlockTimeTicks )
 {
-    NetworkBufferDescriptor_t * pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) malloc( sizeof( NetworkBufferDescriptor_t ) );
+    NetworkBufferDescriptor_t * pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
 
     if( pxNetworkBuffer != NULL )
     {
-        pxNetworkBuffer->pucEthernetBuffer = malloc( xRequestedSizeBytes + ipUDP_PAYLOAD_IP_TYPE_OFFSET );
+        pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xRequestedSizeBytes + ipBUFFER_PADDING + ipUDP_PAYLOAD_IP_TYPE_OFFSET );
 
         if( pxNetworkBuffer->pucEthernetBuffer == NULL )
         {
@@ -129,7 +129,7 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS
         }
         else
         {
-            pxNetworkBuffer->pucEthernetBuffer = ( ( uint8_t * ) pxNetworkBuffer->pucEthernetBuffer ) + ipUDP_PAYLOAD_IP_TYPE_OFFSET;
+            pxNetworkBuffer->pucEthernetBuffer = ( ( uint8_t * ) pxNetworkBuffer->pucEthernetBuffer ) + ipBUFFER_PADDING + ipUDP_PAYLOAD_IP_TYPE_OFFSET;
             pxNetworkBuffer->xDataLength = xRequestedSizeBytes;
         }
     }
@@ -137,6 +137,19 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS
     return pxNetworkBuffer;
 }
 
+/*
+ * In this function, it only allocates network buffer by pxGetNetworkBufferWithDescriptor
+ * stub function above here. In this case, we should free both network buffer descriptor and pucEthernetBuffer.
+ */
+void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer )
+{
+    __CPROVER_assert( pxNetworkBuffer != NULL,
+                      "Precondition: pxNetworkBuffer != NULL" );
+
+    free( pxNetworkBuffer->pucEthernetBuffer - ( ipUDP_PAYLOAD_IP_TYPE_OFFSET + ipBUFFER_PADDING ) );
+    free( pxNetworkBuffer );
+}
+
 Socket_t DNS_CreateSocket( TickType_t uxReadTimeout_ticks )
 {
     Socket_t xSock = safeMalloc( sizeof( struct xSOCKET ) );
@@ -144,6 +157,98 @@ Socket_t DNS_CreateSocket( TickType_t uxReadTimeout_ticks )
     return xSock;
 }
 
+void DNS_CloseSocket( Socket_t xDNSSocket )
+{
+    __CPROVER_assert( xDNSSocket != NULL, "The xDNSSocket cannot be NULL." );
+    free( xDNSSocket );
+}
+
+/****************************************************************
+* Abstract  DNS_BindSocket
+*
+* We stub out this function with return constraint of true or false
+*
+****************************************************************/
+BaseType_t DNS_BindSocket( Socket_t xSocket,
+                           uint16_t usPort )
+{
+    BaseType_t xReturn;
+
+    __CPROVER_assume( xReturn == pdTRUE || xReturn == pdFALSE );
+
+    return xReturn;
+}
+
+/****************************************************************
+* Abstract  DNS_SendRequest
+*
+* We stub out this function with return constraint of true or false
+*
+****************************************************************/
+uint32_t DNS_SendRequest( Socket_t xDNSSocket,
+                          struct freertos_sockaddr * xAddress,
+                          struct xDNSBuffer * pxDNSBuf )
+{
+    uint32_t ret;
+
+    __CPROVER_assume( ret >= 0 );
+    __CPROVER_assume( ret <= 1 );
+
+    return ret;
+}
+
+/****************************************************************
+* Abstract DNS_ReadReply
+*
+* We stub out this function which returned a dns_buffer filled with random data
+*
+****************************************************************/
+BaseType_t DNS_ReadReply( ConstSocket_t xDNSSocket,
+                          struct freertos_sockaddr * xAddress,
+                          struct xDNSBuffer * pxDNSBuf )
+{
+    BaseType_t ret;
+    int len;
+    NetworkBufferDescriptor_t * pxNetworkBuffer;
+
+    __CPROVER_assume( ( len > sizeof( DNSMessage_t ) ) && ( len < ipconfigNETWORK_MTU ) );
+
+    if( nondet_bool() )
+    {
+        pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( len, 0 );
+        __CPROVER_assume( pxNetworkBuffer != NULL );
+
+        pxDNSBuf->pucPayloadBuffer = pxNetworkBuffer->pucEthernetBuffer;
+        pxDNSBuf->uxPayloadLength = len;
+        __CPROVER_assume( pxDNSBuf->pucPayloadBuffer != NULL );
+
+        __CPROVER_havoc_slice( pxDNSBuf->pucPayloadBuffer, pxDNSBuf->uxPayloadLength );
+
+        ret = len;
+    }
+    else
+    {
+        __CPROVER_assume( ret < 0 );
+    }
+
+    return ret;
+}
+
+/* Function xDNSSetCallBack is proven to be correct separately. */
+BaseType_t xDNSSetCallBack( const char * pcHostName,
+                            void * pvSearchID,
+                            FOnDNSEvent pCallbackFunction,
+                            TickType_t xTimeout,
+                            TickType_t xIdentifier,
+                            BaseType_t xIsIPv6 )
+{
+    BaseType_t xReturn;
+
+    __CPROVER_assume( xReturn == pdTRUE || xReturn == pdFALSE );
+
+    return xReturn;
+}
+
 uint32_t Prepare_CacheLookup( const char * pcHostName,
                               BaseType_t xFamily,
                               struct freertos_addrinfo ** ppxAddressInfo )
diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json
index f67cb0a11..4f9571a34 100644
--- a/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json
+++ b/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json
@@ -24,11 +24,13 @@
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
-    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto"
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto"
   ],
   "DEF":
   [

From e35623726fdb5dc77b03c66be5836dda22f33644 Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Fri, 12 Jul 2024 03:33:13 +0000
Subject: [PATCH 20/36] Fix prepareReplyDNSMessage CBMC test

---
 test/cbmc/proofs/DNS/prepareReplyDNSMessage/Makefile.json | 1 +
 1 file changed, 1 insertion(+)

diff --git a/test/cbmc/proofs/DNS/prepareReplyDNSMessage/Makefile.json b/test/cbmc/proofs/DNS/prepareReplyDNSMessage/Makefile.json
index f4f366afb..29e55e2b6 100644
--- a/test/cbmc/proofs/DNS/prepareReplyDNSMessage/Makefile.json
+++ b/test/cbmc/proofs/DNS/prepareReplyDNSMessage/Makefile.json
@@ -10,6 +10,7 @@
     [
       "$(ENTRY)_harness.goto",
       "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
+      "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
       "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto",
       "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto"
     ],

From d9cb180cec007f640c2580c1f9bda70afe467970 Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Fri, 12 Jul 2024 03:42:59 +0000
Subject: [PATCH 21/36] Fix IP CBMC test

---
 .../proofs/IP/ProcessEthernetPacket/Makefile.json  |  5 ++++-
 .../cbmc/proofs/IP/SendEventToIPTask/Makefile.json |  4 +++-
 .../SendEventToIPTask/SendEventToIPTask_harness.c  | 10 ++++++++++
 test/cbmc/stubs/freertos_kernel_api.c              | 14 ++++++++++++++
 4 files changed, 31 insertions(+), 2 deletions(-)

diff --git a/test/cbmc/proofs/IP/ProcessEthernetPacket/Makefile.json b/test/cbmc/proofs/IP/ProcessEthernetPacket/Makefile.json
index 4a2b35b44..101f63983 100644
--- a/test/cbmc/proofs/IP/ProcessEthernetPacket/Makefile.json
+++ b/test/cbmc/proofs/IP/ProcessEthernetPacket/Makefile.json
@@ -12,6 +12,9 @@
   [
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto"
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto"
   ]
 }
diff --git a/test/cbmc/proofs/IP/SendEventToIPTask/Makefile.json b/test/cbmc/proofs/IP/SendEventToIPTask/Makefile.json
index 30727432c..dfffab176 100644
--- a/test/cbmc/proofs/IP/SendEventToIPTask/Makefile.json
+++ b/test/cbmc/proofs/IP/SendEventToIPTask/Makefile.json
@@ -36,6 +36,8 @@
   [
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
-    "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto"
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto"
   ]
 }
diff --git a/test/cbmc/proofs/IP/SendEventToIPTask/SendEventToIPTask_harness.c b/test/cbmc/proofs/IP/SendEventToIPTask/SendEventToIPTask_harness.c
index 706bdb905..665d0ee92 100644
--- a/test/cbmc/proofs/IP/SendEventToIPTask/SendEventToIPTask_harness.c
+++ b/test/cbmc/proofs/IP/SendEventToIPTask/SendEventToIPTask_harness.c
@@ -36,6 +36,16 @@
 #include "FreeRTOS_IP.h"
 #include "FreeRTOS_IP_Private.h"
 
+/* Abstraction of xIsCallingFromIPTask */
+BaseType_t xIsCallingFromIPTask( void )
+{
+    BaseType_t xReturn;
+
+    __CPROVER_assume( ( xReturn == pdTRUE ) || ( xReturn == pdFALSE ) );
+
+    return xReturn;
+}
+
 /* The harness test proceeds to call SendEventToIPTask with an unconstrained value */
 void harness()
 {
diff --git a/test/cbmc/stubs/freertos_kernel_api.c b/test/cbmc/stubs/freertos_kernel_api.c
index 25ea16dd6..01d1329b1 100644
--- a/test/cbmc/stubs/freertos_kernel_api.c
+++ b/test/cbmc/stubs/freertos_kernel_api.c
@@ -98,6 +98,20 @@ BaseType_t xQueueGenericSend( QueueHandle_t xQueue,
 
 /****************************************************************/
 
+/****************************************************************
+* Abstract uxQueueMessagesWaiting
+****************************************************************/
+UBaseType_t uxQueueMessagesWaiting( const QueueHandle_t xQueue )
+{
+    UBaseType_t uxReturn;
+
+    __CPROVER_assume( uxReturn <= 2 );
+
+    return uxReturn;
+}
+
+/****************************************************************/
+
 /****************************************************************
 * Abstract vTaskSetTimeOutState
 ****************************************************************/

From 0978d6770406f000357f6951be4d0ebbc0284ead Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Fri, 12 Jul 2024 05:08:02 +0000
Subject: [PATCH 22/36] Fix ND CBMC test

---
 .../prvProcessICMPMessage_IPv6/Makefile.json  |  7 ++-
 .../ProcessICMPMessage_IPv6_harness.c         | 51 ++++++++++++------
 .../ND/prvReturnICMP_IPv6/Makefile.json       |  7 ++-
 .../ReturnICMP_IPv6_harness.c                 | 52 +++++++++++++------
 4 files changed, 79 insertions(+), 38 deletions(-)

diff --git a/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/Makefile.json b/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/Makefile.json
index 09f7d0beb..151aefe2e 100644
--- a/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/Makefile.json
+++ b/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/Makefile.json
@@ -8,8 +8,11 @@
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ND.goto"
-
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ND.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto"
   ],
   "DEF":
   [
diff --git a/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/ProcessICMPMessage_IPv6_harness.c b/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/ProcessICMPMessage_IPv6_harness.c
index 990736bc7..3efb55b4c 100644
--- a/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/ProcessICMPMessage_IPv6_harness.c
+++ b/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/ProcessICMPMessage_IPv6_harness.c
@@ -37,7 +37,6 @@
 #include "FreeRTOS_ND.h"
 
 /* CBMC includes. */
-#include "../../utility/memory_assignments.c"
 #include "cbmc.h"
 
 extern NDCacheRow_t xNDCache[ ipconfigND_CACHE_ENTRIES ];
@@ -70,6 +69,12 @@ void vReceiveNA( const NetworkBufferDescriptor_t * pxNetworkBuffer )
     __CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." );
 }
 
+/* This function has been tested separately. Therefore, we assume that the implementation is correct. */
+void vReceiveRA( const NetworkBufferDescriptor_t * pxNetworkBuffer )
+{
+    __CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." );
+}
+
 /* This function has been tested separately. Therefore, we assume that the implementation is correct. */
 BaseType_t xSendEventStructToIPTask( const IPStackEvent_t * pxEvent,
                                      TickType_t uxTimeout )
@@ -103,7 +108,7 @@ NetworkEndPoint_t * FreeRTOS_InterfaceEPInSameSubnet_IPv6( const NetworkInterfac
 
     pxEndPoints = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
 
-    if( ensure_memory_is_valid( pxEndPoints, sizeof( NetworkEndPoint_t ) ) )
+    if( ( pxEndPoints ) && __CPROVER_w_ok( pxEndPoints, sizeof( NetworkEndPoint_t ) ) )
     {
         /* Interface init. */
         pxEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) );
@@ -116,21 +121,32 @@ NetworkEndPoint_t * FreeRTOS_InterfaceEPInSameSubnet_IPv6( const NetworkInterfac
     return pxEndPoints;
 }
 
+size_t uxIPHeaderSizePacket( const NetworkBufferDescriptor_t * pxNetworkBuffer )
+{
+    size_t uxResult;
+    
+    __CPROVER_assume( ( uxResult == ipSIZE_OF_IPv4_HEADER ) || ( uxResult == ipSIZE_OF_IPv6_HEADER ) );
+
+    return uxResult;
+}
+
 void harness()
 {
-    NetworkBufferDescriptor_t * pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated();
+    NetworkBufferDescriptor_t * pxNetworkBuffer;
     uint32_t ulLen;
     uint16_t usEthernetBufferSize;
-    NetworkBufferDescriptor_t xLocalBuffer;
+    NetworkBufferDescriptor_t * pxLocalARPWaitingNetworkBuffer;
+
+    __CPROVER_assume( ( ulLen >= sizeof( ICMPPacket_IPv6_t ) ) && ( ulLen < ipconfigNETWORK_MTU ) );
+
+    pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( ulLen, 0 );
 
     /* The code does not expect pxNetworkBuffer to be NULL. */
     __CPROVER_assume( pxNetworkBuffer != NULL );
-
-    __CPROVER_assume( ( ulLen >= sizeof( ICMPPacket_IPv6_t ) ) && ( ulLen < ipconfigNETWORK_MTU ) );
+    __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
+    __CPROVER_havoc_slice( pxNetworkBuffer->pucEthernetBuffer, ulLen );
 
     pxNetworkBuffer->xDataLength = ulLen;
-    pxNetworkBuffer->pucEthernetBuffer = safeMalloc( ulLen );
-    __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. */
@@ -147,19 +163,20 @@ void harness()
         /* The packet must at least be as big as an IPv6 Packet. The size is not
          * checked in the function as the pointer is stored by the IP-task itself
          * and therefore it will always be of the required size. */
-        __CPROVER_assume( usEthernetBufferSize >= sizeof( IPPacket_IPv6_t ) );
-
-        /* Add matching data length to the network buffer descriptor. */
-        __CPROVER_assume( xLocalBuffer.xDataLength == usEthernetBufferSize );
-
-        xLocalBuffer.pucEthernetBuffer = safeMalloc( usEthernetBufferSize );
+        __CPROVER_assume( ( usEthernetBufferSize >= sizeof( IPPacket_IPv6_t ) ) && ( usEthernetBufferSize < ipconfigNETWORK_MTU ) );
+        pxLocalARPWaitingNetworkBuffer = pxGetNetworkBufferWithDescriptor( usEthernetBufferSize, 0 );
 
         /* Since this pointer is maintained by the IP-task, either the pointer
-         * pxARPWaitingNetworkBuffer will be NULL or xLocalBuffer.pucEthernetBuffer
+         * pxARPWaitingNetworkBuffer will be NULL or pxLocalARPWaitingNetworkBuffer.pucEthernetBuffer
          * will be non-NULL. */
-        __CPROVER_assume( xLocalBuffer.pucEthernetBuffer != NULL );
+        __CPROVER_assume( pxLocalARPWaitingNetworkBuffer != NULL );
+        __CPROVER_assume( pxLocalARPWaitingNetworkBuffer->pucEthernetBuffer != NULL );
+        __CPROVER_havoc_slice( pxLocalARPWaitingNetworkBuffer->pucEthernetBuffer, usEthernetBufferSize );
+
+        /* Add matching data length to the network buffer descriptor. */
+        pxLocalARPWaitingNetworkBuffer->xDataLength = usEthernetBufferSize;
 
-        pxARPWaitingNetworkBuffer = &xLocalBuffer;
+        pxARPWaitingNetworkBuffer = pxLocalARPWaitingNetworkBuffer;
     }
     else
     {
diff --git a/test/cbmc/proofs/ND/prvReturnICMP_IPv6/Makefile.json b/test/cbmc/proofs/ND/prvReturnICMP_IPv6/Makefile.json
index cdc3a4f0a..47de0cd15 100644
--- a/test/cbmc/proofs/ND/prvReturnICMP_IPv6/Makefile.json
+++ b/test/cbmc/proofs/ND/prvReturnICMP_IPv6/Makefile.json
@@ -8,8 +8,11 @@
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ND.goto"
-
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ND.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto"
   ],
   "INC":
   [
diff --git a/test/cbmc/proofs/ND/prvReturnICMP_IPv6/ReturnICMP_IPv6_harness.c b/test/cbmc/proofs/ND/prvReturnICMP_IPv6/ReturnICMP_IPv6_harness.c
index b40437501..1c072f6f1 100644
--- a/test/cbmc/proofs/ND/prvReturnICMP_IPv6/ReturnICMP_IPv6_harness.c
+++ b/test/cbmc/proofs/ND/prvReturnICMP_IPv6/ReturnICMP_IPv6_harness.c
@@ -37,7 +37,6 @@
 #include "FreeRTOS_ND.h"
 
 /* CBMC includes. */
-#include "../../utility/memory_assignments.c"
 #include "cbmc.h"
 
 extern NDCacheRow_t xNDCache[ ipconfigND_CACHE_ENTRIES ];
@@ -72,6 +71,12 @@ void vReceiveNA( const NetworkBufferDescriptor_t * pxNetworkBuffer )
     __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "The Ethernet buffer cannot be NULL." );
 }
 
+/* This function has been tested separately. Therefore, we assume that the implementation is correct. */
+void vReceiveRA( const NetworkBufferDescriptor_t * pxNetworkBuffer )
+{
+    __CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." );
+}
+
 /* This function has been tested separately. Therefore, we assume that the implementation is correct. */
 BaseType_t xSendEventStructToIPTask( const IPStackEvent_t * pxEvent,
                                      TickType_t uxTimeout )
@@ -106,7 +111,7 @@ NetworkEndPoint_t * FreeRTOS_InterfaceEPInSameSubnet_IPv6( const NetworkInterfac
 
     pxEndPoints = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
 
-    if( ensure_memory_is_valid( pxEndPoints, sizeof( NetworkEndPoint_t ) ) )
+    if( ( pxEndPoints ) && __CPROVER_w_ok( pxEndPoints, sizeof( NetworkEndPoint_t ) ) )
     {
         /* Interface init. */
         pxEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) );
@@ -119,21 +124,33 @@ NetworkEndPoint_t * FreeRTOS_InterfaceEPInSameSubnet_IPv6( const NetworkInterfac
     return pxEndPoints;
 }
 
+size_t uxIPHeaderSizePacket( const NetworkBufferDescriptor_t * pxNetworkBuffer )
+{
+    size_t uxResult;
+    
+    __CPROVER_assume( ( uxResult == ipSIZE_OF_IPv4_HEADER ) || ( uxResult == ipSIZE_OF_IPv6_HEADER ) );
+
+    return uxResult;
+}
+
 void harness()
 {
-    NetworkBufferDescriptor_t * pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated();
+    NetworkBufferDescriptor_t * pxNetworkBuffer;
     uint32_t ulLen;
-    NetworkBufferDescriptor_t xLocalBuffer;
+    NetworkBufferDescriptor_t *pxLocalARPWaitingNetworkBuffer;
     uint16_t usEthernetBufferSize;
 
-    /* The code does not expect both of these to be equal to NULL at the same time. */
-    __CPROVER_assume( pxNetworkBuffer != NULL );
-
     __CPROVER_assume( ( ulLen >= sizeof( ICMPPacket_IPv6_t ) ) && ( ulLen < ipconfigNETWORK_MTU ) );
+    
+    pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( ulLen, 0 );
+
+    /* The code does not expect pxNetworkBuffer to be NULL. */
+    __CPROVER_assume( pxNetworkBuffer != NULL );
 
     pxNetworkBuffer->xDataLength = ulLen;
     pxNetworkBuffer->pucEthernetBuffer = safeMalloc( ulLen );
-    __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer );
+    __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
+    __CPROVER_havoc_slice( pxNetworkBuffer->pucEthernetBuffer, ulLen );
 
     /* 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. */
@@ -149,19 +166,20 @@ void harness()
     /* The packet must at least be as big as an IPv6 Packet. The size is not
      * checked in the function as the pointer is stored by the IP-task itself
      * and therefore it will always be of the required size. */
-    __CPROVER_assume( usEthernetBufferSize >= sizeof( IPPacket_IPv6_t ) );
-
-    /* Add matching data length to the network buffer descriptor. */
-    __CPROVER_assume( xLocalBuffer.xDataLength == usEthernetBufferSize );
-
-    xLocalBuffer.pucEthernetBuffer = safeMalloc( usEthernetBufferSize );
+    __CPROVER_assume( ( usEthernetBufferSize >= sizeof( IPPacket_IPv6_t ) ) && ( usEthernetBufferSize < ipconfigNETWORK_MTU ) );
+    pxLocalARPWaitingNetworkBuffer = pxGetNetworkBufferWithDescriptor( usEthernetBufferSize, 0 );
 
     /* Since this pointer is maintained by the IP-task, either the pointer
-     * pxARPWaitingNetworkBuffer will be NULL or xLocalBuffer.pucEthernetBuffer
+     * pxARPWaitingNetworkBuffer will be NULL or pxLocalARPWaitingNetworkBuffer.pucEthernetBuffer
      * will be non-NULL. */
-    __CPROVER_assume( xLocalBuffer.pucEthernetBuffer != NULL );
+    __CPROVER_assume( pxLocalARPWaitingNetworkBuffer != NULL );
+    __CPROVER_assume( pxLocalARPWaitingNetworkBuffer->pucEthernetBuffer != NULL );
+    __CPROVER_havoc_slice( pxLocalARPWaitingNetworkBuffer->pucEthernetBuffer, usEthernetBufferSize );
+
+    /* Add matching data length to the network buffer descriptor. */
+    pxLocalARPWaitingNetworkBuffer->xDataLength = usEthernetBufferSize;
 
-    pxARPWaitingNetworkBuffer = &xLocalBuffer;
+    pxARPWaitingNetworkBuffer = pxLocalARPWaitingNetworkBuffer;
 
     prvProcessICMPMessage_IPv6( pxNetworkBuffer );
 }

From 3efe16e2a932c2cfa3c35a319cc960de661f7148 Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Fri, 12 Jul 2024 08:34:22 +0000
Subject: [PATCH 23/36] Fix RA CBMC test

---
 test/cbmc/proofs/RA/vReceiveRA/Makefile.json  |  8 ++-
 .../proofs/RA/vReceiveRA/ReceiveRA_harness.c  | 60 ++++++++++++++-----
 .../RA/vReceiveRA_ReadReply/Makefile.json     |  1 +
 3 files changed, 53 insertions(+), 16 deletions(-)

diff --git a/test/cbmc/proofs/RA/vReceiveRA/Makefile.json b/test/cbmc/proofs/RA/vReceiveRA/Makefile.json
index 8b995fc8d..1a4edbd46 100644
--- a/test/cbmc/proofs/RA/vReceiveRA/Makefile.json
+++ b/test/cbmc/proofs/RA/vReceiveRA/Makefile.json
@@ -4,6 +4,7 @@
   [
     "--unwind 2",
     "--unwindset FreeRTOS_NextEndPoint.0:1",
+    "--unwindset FreeRTOS_CreateIPv6Address.0:5",
     "--nondet-static"
   ],
   "OPT":
@@ -13,8 +14,13 @@
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_RA.goto"
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_RA.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ND.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto"
 
   ],
   "INC":
diff --git a/test/cbmc/proofs/RA/vReceiveRA/ReceiveRA_harness.c b/test/cbmc/proofs/RA/vReceiveRA/ReceiveRA_harness.c
index e7f6cf505..424c45832 100644
--- a/test/cbmc/proofs/RA/vReceiveRA/ReceiveRA_harness.c
+++ b/test/cbmc/proofs/RA/vReceiveRA/ReceiveRA_harness.c
@@ -37,7 +37,6 @@
 #include "FreeRTOS_ND.h"
 
 /* CBMC includes. */
-#include "../../utility/memory_assignments.c"
 #include "cbmc.h"
 
 /* This function has been tested separately. Therefore, we assume that the implementation is correct. */
@@ -45,6 +44,11 @@ ICMPPrefixOption_IPv6_t * __CPROVER_file_local_FreeRTOS_RA_c_vReceiveRA_ReadRepl
 {
     ICMPPrefixOption_IPv6_t * pxPrefixOption = safeMalloc( sizeof( ICMPPrefixOption_IPv6_t ) );
 
+    if( pxPrefixOption )
+    {
+        __CPROVER_assume( ( pxPrefixOption->ucPrefixLength > 0U ) && ( pxPrefixOption->ucPrefixLength <= ( 8U * ipSIZE_OF_IPv6_ADDRESS ) ) );
+    }
+
     return pxPrefixOption;
 }
 
@@ -75,30 +79,56 @@ void vNDSendRouterSolicitation( NetworkBufferDescriptor_t * pxNetworkBuffer,
     __CPROVER_assert( pxIPAddress != NULL, "The pxIPAddress cannot be NULL." );
 }
 
-void harness()
+/* The checksum generation is stubbed out since the actual checksum
+ * does not matter. The stub will return an indeterminate value each time. */
+uint16_t usGenerateProtocolChecksum( const uint8_t * const pucEthernetBuffer,
+                                     size_t uxBufferLength,
+                                     BaseType_t xOutgoingPacket )
 {
-    NetworkBufferDescriptor_t * pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated();
-    NetworkInterface_t * pxInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) );
-    uint32_t ulLen;
+    __CPROVER_assert( pucEthernetBuffer != NULL, "Ethernet buffer cannot be NULL" );
 
-    /* The code does not expect pxNetworkBuffer to be NULL. */
-    __CPROVER_assume( pxNetworkBuffer != NULL );
-
-    __CPROVER_assume( ( ulLen >= sizeof( ICMPPacket_IPv6_t ) ) && ( ulLen < ipconfigNETWORK_MTU ) );
-    pxNetworkBuffer->pucEthernetBuffer = safeMalloc( ulLen );
-    __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
+    /* Return an indeterminate value. */
+    return ( uint16_t ) nondet_uint32();
+}
 
-    pxNetworkBuffer->pxInterface = safeMalloc( sizeof( NetworkInterface_t ) );
-    __CPROVER_assume( pxNetworkBuffer->pxInterface != NULL );
+/* vReturnEthernetFrame() is proved separately */
+void vReturnEthernetFrame( NetworkBufferDescriptor_t * pxNetworkBuffer,
+                           BaseType_t xReleaseAfterSend )
+{
+    __CPROVER_assert( pxNetworkBuffer != NULL, "xNetworkBuffer != NULL" );
+    __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "pxNetworkBuffer->pucEthernetBuffer != NULL" );
+    __CPROVER_assert( __CPROVER_r_ok( pxNetworkBuffer->pucEthernetBuffer, pxNetworkBuffer->xDataLength ), "Data must be valid" );
+}
 
-    pxNetworkBuffer->pxEndPoint = safeMalloc( sizeof( NetworkEndPoint_t ) );
+void harness()
+{
+    NetworkBufferDescriptor_t * pxNetworkBuffer;
+    NetworkInterface_t * pxInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) );
+    uint32_t ulLen;
 
     /* Initialize global Endpoint variable  */
     pxNetworkEndPoints = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
     __CPROVER_assume( pxNetworkEndPoints != NULL );
-    pxNetworkEndPoints->pxNetworkInterface = pxNetworkBuffer->pxInterface;
+    pxNetworkEndPoints->pxNetworkInterface = safeMalloc( sizeof( NetworkInterface_t ) );
+    __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
     __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
     pxNetworkEndPoints->pxNext = NULL;
 
+    /* Initialize network buffer. */
+    __CPROVER_assume( ( ulLen >= sizeof( ICMPPacket_IPv6_t ) ) && ( ulLen < ipconfigNETWORK_MTU ) );
+
+    pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( ulLen, 0 );
+
+    /* The code does not expect pxNetworkBuffer to be NULL. */
+    __CPROVER_assume( pxNetworkBuffer != NULL );
+    __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
+    __CPROVER_havoc_slice( pxNetworkBuffer->pucEthernetBuffer, ulLen );
+
+    pxNetworkBuffer->pxInterface = pxNetworkEndPoints->pxNetworkInterface;
+    pxNetworkBuffer->pxEndPoint = pxNetworkEndPoints;
+
+    /* The prefix length must be equal to or less than 128 to avoid assertion in FreeRTOS_CreateIPv6Address(). */
+    __CPROVER_assume( ( pxNetworkEndPoints->ipv6_settings.uxPrefixLength > 0U ) && ( pxNetworkEndPoints->ipv6_settings.uxPrefixLength <= ( 8U * ipSIZE_OF_IPv6_ADDRESS ) ) );
+
     vReceiveRA( pxNetworkBuffer );
 }
diff --git a/test/cbmc/proofs/RA/vReceiveRA_ReadReply/Makefile.json b/test/cbmc/proofs/RA/vReceiveRA_ReadReply/Makefile.json
index 61d93b3d5..91ff52732 100644
--- a/test/cbmc/proofs/RA/vReceiveRA_ReadReply/Makefile.json
+++ b/test/cbmc/proofs/RA/vReceiveRA_ReadReply/Makefile.json
@@ -12,6 +12,7 @@
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_RA.goto"
 
   ],

From ecbdb8ba1fc943fdd3eedc9437b858d7fe710320 Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Fri, 12 Jul 2024 08:37:13 +0000
Subject: [PATCH 24/36] Fix Routing CBMC test

---
 .../MatchingEndpoint/MatchingEndpoint_harness.c        | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/test/cbmc/proofs/Routing/MatchingEndpoint/MatchingEndpoint_harness.c b/test/cbmc/proofs/Routing/MatchingEndpoint/MatchingEndpoint_harness.c
index dbcde05c0..1496562b1 100644
--- a/test/cbmc/proofs/Routing/MatchingEndpoint/MatchingEndpoint_harness.c
+++ b/test/cbmc/proofs/Routing/MatchingEndpoint/MatchingEndpoint_harness.c
@@ -39,6 +39,16 @@
 #include "../../utility/memory_assignments.c"
 #include "cbmc.h"
 
+/* Abstraction of xIsIPv6Loopback returns either true or false. */
+BaseType_t xIsIPv6Loopback( const IPv6_Address_t * pxAddress )
+{
+    BaseType_t xReturn;
+
+    __CPROVER_assume( xReturn == pdTRUE || xReturn == pdFALSE );
+
+    return xReturn;
+}
+
 void harness()
 {
     NetworkInterface_t * pxNetworkInterface = safeMalloc( sizeof( NetworkInterface_t ) );

From d3e43b51a53545b9ffbfa77465b6bc0b09901e0c Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Fri, 12 Jul 2024 09:08:20 +0000
Subject: [PATCH 25/36] Fix lTCPAddRxdata CBMC test

---
 .../lTCPAddRxdata/TCPAddRxdata_harness.c      | 37 ++++++++++++++++++-
 1 file changed, 36 insertions(+), 1 deletion(-)

diff --git a/test/cbmc/proofs/Socket/lTCPAddRxdata/TCPAddRxdata_harness.c b/test/cbmc/proofs/Socket/lTCPAddRxdata/TCPAddRxdata_harness.c
index 6e0b9278a..4fefc1d10 100644
--- a/test/cbmc/proofs/Socket/lTCPAddRxdata/TCPAddRxdata_harness.c
+++ b/test/cbmc/proofs/Socket/lTCPAddRxdata/TCPAddRxdata_harness.c
@@ -34,11 +34,44 @@ void * pvPortMallocLarge( size_t xWantedSize )
     return safeMalloc( xWantedSize );
 }
 
+size_t uxStreamBufferFrontSpace( const StreamBuffer_t * const pxBuffer )
+{
+    size_t uxReturn;
+    return uxReturn;
+}
+
+BaseType_t xSendEventToIPTask( eIPEvent_t eEvent )
+{
+    BaseType_t xReturn;
+
+    __CPROVER_assume( ( xReturn == pdTRUE ) || ( xReturn == pdFALSE ) );
+
+    return xReturn;
+}
+
+void vTCPStateChange( FreeRTOS_Socket_t * pxSocket,
+                      enum eTCP_STATE eTCPState )
+{
+}
+
+size_t uxStreamBufferAdd( StreamBuffer_t * const pxBuffer,
+                          size_t uxOffset,
+                          const uint8_t * const pucData,
+                          size_t uxByteCount )
+{
+    size_t uxReturn;
+
+    __CPROVER_assert( __CPROVER_r_ok( pucData, uxByteCount ), "Data pointer must be valid to read" );
+    __CPROVER_assume( uxReturn <= uxByteCount );
+
+    return uxReturn;
+}
+
 void harness()
 {
     FreeRTOS_Socket_t * pxSocket = ensure_FreeRTOS_Socket_t_is_allocated();
     size_t uxOffset;
-    const uint8_t * pcData;
+    const uint8_t * pcData = NULL;
     uint32_t ulByteCount;
 
     /* This function expect socket to be not NULL, as it has been validated previously */
@@ -48,7 +81,9 @@ void harness()
     __CPROVER_assume( pxSocket->u.xTCP.uxRxStreamSize >= 0 && pxSocket->u.xTCP.uxRxStreamSize < ipconfigTCP_RX_BUFFER_LENGTH );
     __CPROVER_assume( pxSocket->u.xTCP.uxTxStreamSize >= 0 && pxSocket->u.xTCP.uxTxStreamSize < ipconfigTCP_TX_BUFFER_LENGTH );
 
+    __CPROVER_assume( ulByteCount > 0U );
     pcData = safeMalloc( ulByteCount );
+    __CPROVER_assume( pcData != NULL );
 
     lTCPAddRxdata( pxSocket, uxOffset, pcData, ulByteCount );
 }

From a4a73273c86a369f4bd8eb9971c426b939c5c5a4 Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Fri, 12 Jul 2024 09:16:58 +0000
Subject: [PATCH 26/36] Fix Socket CBMC test

---
 .../Makefile.json                             |  3 ++-
 .../Socket/vSocketClose/Configurations.json   |  1 +
 test/cbmc/stubs/freertos_kernel_api.c         | 20 +++++++++++++++++++
 3 files changed, 23 insertions(+), 1 deletion(-)

diff --git a/test/cbmc/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/Makefile.json b/test/cbmc/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/Makefile.json
index 379ae7a39..336e6d2ec 100644
--- a/test/cbmc/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/Makefile.json
+++ b/test/cbmc/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/Makefile.json
@@ -13,7 +13,8 @@
     "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Sockets.goto",
-    "$(ENTRY)_harness.goto"
+    "$(ENTRY)_harness.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto"
   ],
   "INSTFLAGS":
   [
diff --git a/test/cbmc/proofs/Socket/vSocketClose/Configurations.json b/test/cbmc/proofs/Socket/vSocketClose/Configurations.json
index 50df09417..f36f3dc53 100644
--- a/test/cbmc/proofs/Socket/vSocketClose/Configurations.json
+++ b/test/cbmc/proofs/Socket/vSocketClose/Configurations.json
@@ -9,6 +9,7 @@
   [
     "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Sockets.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto",
     "$(ENTRY)_harness.goto"
   ],
   "DEF":
diff --git a/test/cbmc/stubs/freertos_kernel_api.c b/test/cbmc/stubs/freertos_kernel_api.c
index 01d1329b1..fab4c7c98 100644
--- a/test/cbmc/stubs/freertos_kernel_api.c
+++ b/test/cbmc/stubs/freertos_kernel_api.c
@@ -81,6 +81,26 @@ EventBits_t xEventGroupSetBits( EventGroupHandle_t xEventGroup,
 
 /****************************************************************/
 
+/****************************************************************
+* Abstract xEventGroupSetBits
+****************************************************************/
+void vEventGroupDelete( EventGroupHandle_t xEventGroup )
+{
+}
+
+/****************************************************************/
+
+/****************************************************************
+* Abstract xEventGroupSetBits
+****************************************************************/
+EventGroupHandle_t xEventGroupCreate( void )
+{
+    EventGroupHandle_t xReturn;
+    return xReturn;
+}
+
+/****************************************************************/
+
 /****************************************************************
 * Abstract xQueueGenericSend
 ****************************************************************/

From 853d220dd7aed03637dda6c4808691fe52cc2374 Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Tue, 16 Jul 2024 06:47:43 +0000
Subject: [PATCH 27/36] Fix TCP CBMC test

---
 .../proofs/TCP/prvHandleListen/Makefile.json  |   2 +-
 .../prvHandleListen/prvHandleListen_harness.c |  60 +++++
 .../TCP/prvHandleListen_IPv6/Makefile.json    |   2 +-
 .../prvHandleListen_IPv6_harness.c            |  60 +++++
 .../cbmc/proofs/TCP/prvSendData/Makefile.json |   3 +-
 .../proofs/TCP/prvSendData/SendData_harness.c |  64 ++++-
 .../TCP/prvTCPHandleState/Makefile.json       |  11 +-
 .../TCPHandleState_harness.c                  | 234 +++++++++++++++---
 .../TCP/prvTCPPrepareSend/Makefile.json       |   8 +-
 .../TCPPrepareSend_harness.c                  | 120 ++++++---
 .../TCP/prvTCPReturnPacket/Makefile.json      |   9 +-
 .../TCPReturnPacket_harness.c                 |  95 +++++--
 .../TCP/prvTCPReturnPacket_IPv6/Makefile.json |   9 +-
 .../TCPReturnPacket_IPv6_harness.c            | 101 ++++++--
 test/cbmc/stubs/freertos_api.c                |  28 +++
 15 files changed, 684 insertions(+), 122 deletions(-)

diff --git a/test/cbmc/proofs/TCP/prvHandleListen/Makefile.json b/test/cbmc/proofs/TCP/prvHandleListen/Makefile.json
index 856e50c30..ab47b60c1 100644
--- a/test/cbmc/proofs/TCP/prvHandleListen/Makefile.json
+++ b/test/cbmc/proofs/TCP/prvHandleListen/Makefile.json
@@ -9,6 +9,7 @@
   [
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_State_Handling.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_State_Handling_IPv4.goto"
   ],
@@ -19,7 +20,6 @@
   ],
   "INSTFLAGS":
   [
-    "--remove-function-body prvTCPSendReset"
   ],
   "INC":
   [
diff --git a/test/cbmc/proofs/TCP/prvHandleListen/prvHandleListen_harness.c b/test/cbmc/proofs/TCP/prvHandleListen/prvHandleListen_harness.c
index a74229372..3fa5aadd8 100644
--- a/test/cbmc/proofs/TCP/prvHandleListen/prvHandleListen_harness.c
+++ b/test/cbmc/proofs/TCP/prvHandleListen/prvHandleListen_harness.c
@@ -53,6 +53,66 @@ Socket_t FreeRTOS_socket( BaseType_t xDomain,
     return ensure_FreeRTOS_Socket_t_is_allocated();
 }
 
+BaseType_t vSocketBind( FreeRTOS_Socket_t * pxSocket,
+                        struct freertos_sockaddr * pxBindAddress,
+                        size_t uxAddressLength,
+                        BaseType_t xInternal )
+{
+    BaseType_t xRet;
+
+    __CPROVER_assert( pxSocket != NULL,
+                      "FreeRTOS precondition: pxSocket != NULL" );
+    __CPROVER_assert( pxBindAddress != NULL,
+                      "FreeRTOS precondition: pxBindAddress != NULL" );
+
+    return xRet;
+}
+
+void * vSocketClose( FreeRTOS_Socket_t * pxSocket )
+{
+    __CPROVER_assert( pxSocket != NULL, "Closing socket cannot be NULL" );
+
+    return NULL;
+}
+
+BaseType_t prvTCPSendReset( NetworkBufferDescriptor_t * pxNetworkBuffer )
+{
+    BaseType_t xReturn;
+
+    __CPROVER_assume( ( xReturn == pdTRUE ) || ( xReturn == pdFALSE ) );
+
+    return xReturn;
+}
+
+void vTCPStateChange( FreeRTOS_Socket_t * pxSocket,
+                      enum eTCP_STATE eTCPState )
+{
+}
+
+BaseType_t prvTCPCreateWindow( FreeRTOS_Socket_t * pxSocket )
+{
+    BaseType_t xReturn;
+
+    __CPROVER_assume( ( xReturn == pdTRUE ) || ( xReturn == pdFALSE ) );
+
+    return xReturn;
+}
+
+void prvSocketSetMSS( FreeRTOS_Socket_t * pxSocket )
+{
+    __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" );
+}
+
+size_t FreeRTOS_GetLocalAddress( ConstSocket_t xSocket,
+                                 struct freertos_sockaddr * pxAddress )
+{
+    size_t uxReturn;
+
+    __CPROVER_assert( pxAddress != NULL, "pxAddress cannot be NULL" );
+
+    return uxReturn;
+}
+
 void harness()
 {
     size_t xDataLength;
diff --git a/test/cbmc/proofs/TCP/prvHandleListen_IPv6/Makefile.json b/test/cbmc/proofs/TCP/prvHandleListen_IPv6/Makefile.json
index aa1ee4f70..b824b9a39 100644
--- a/test/cbmc/proofs/TCP/prvHandleListen_IPv6/Makefile.json
+++ b/test/cbmc/proofs/TCP/prvHandleListen_IPv6/Makefile.json
@@ -11,6 +11,7 @@
   [
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_State_Handling.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_State_Handling_IPv6.goto"
   ],
@@ -21,7 +22,6 @@
   ],
   "INSTFLAGS":
   [
-    "--remove-function-body prvTCPSendReset"
   ],
   "INC":
   [
diff --git a/test/cbmc/proofs/TCP/prvHandleListen_IPv6/prvHandleListen_IPv6_harness.c b/test/cbmc/proofs/TCP/prvHandleListen_IPv6/prvHandleListen_IPv6_harness.c
index 5134b5bca..8be5891f9 100644
--- a/test/cbmc/proofs/TCP/prvHandleListen_IPv6/prvHandleListen_IPv6_harness.c
+++ b/test/cbmc/proofs/TCP/prvHandleListen_IPv6/prvHandleListen_IPv6_harness.c
@@ -53,6 +53,66 @@ Socket_t FreeRTOS_socket( BaseType_t xDomain,
     return ensure_FreeRTOS_Socket_t_is_allocated();
 }
 
+BaseType_t vSocketBind( FreeRTOS_Socket_t * pxSocket,
+                        struct freertos_sockaddr * pxBindAddress,
+                        size_t uxAddressLength,
+                        BaseType_t xInternal )
+{
+    BaseType_t xRet;
+
+    __CPROVER_assert( pxSocket != NULL,
+                      "FreeRTOS precondition: pxSocket != NULL" );
+    __CPROVER_assert( pxBindAddress != NULL,
+                      "FreeRTOS precondition: pxBindAddress != NULL" );
+
+    return xRet;
+}
+
+void * vSocketClose( FreeRTOS_Socket_t * pxSocket )
+{
+    __CPROVER_assert( pxSocket != NULL, "Closing socket cannot be NULL" );
+
+    return NULL;
+}
+
+void prvSocketSetMSS( FreeRTOS_Socket_t * pxSocket )
+{
+    __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" );
+}
+
+BaseType_t prvTCPSendReset( NetworkBufferDescriptor_t * pxNetworkBuffer )
+{
+    BaseType_t xReturn;
+
+    __CPROVER_assume( ( xReturn == pdTRUE ) || ( xReturn == pdFALSE ) );
+
+    return xReturn;
+}
+
+void vTCPStateChange( FreeRTOS_Socket_t * pxSocket,
+                      enum eTCP_STATE eTCPState )
+{
+}
+
+BaseType_t prvTCPCreateWindow( FreeRTOS_Socket_t * pxSocket )
+{
+    BaseType_t xReturn;
+
+    __CPROVER_assume( ( xReturn == pdTRUE ) || ( xReturn == pdFALSE ) );
+
+    return xReturn;
+}
+
+size_t FreeRTOS_GetLocalAddress( ConstSocket_t xSocket,
+                                 struct freertos_sockaddr * pxAddress )
+{
+    size_t uxReturn;
+
+    __CPROVER_assert( pxAddress != NULL, "pxAddress cannot be NULL" );
+
+    return uxReturn;
+}
+
 void harness()
 {
     size_t xDataLength;
diff --git a/test/cbmc/proofs/TCP/prvSendData/Makefile.json b/test/cbmc/proofs/TCP/prvSendData/Makefile.json
index cfc73e67e..f8b8a29f1 100644
--- a/test/cbmc/proofs/TCP/prvSendData/Makefile.json
+++ b/test/cbmc/proofs/TCP/prvSendData/Makefile.json
@@ -8,7 +8,8 @@
     "OBJS":
     [
       "$(ENTRY)_harness.goto",
-      "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto"
+      "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto",
+      "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto"
     ],
     "INC":
     [
diff --git a/test/cbmc/proofs/TCP/prvSendData/SendData_harness.c b/test/cbmc/proofs/TCP/prvSendData/SendData_harness.c
index 83da8405b..bfd3bde04 100644
--- a/test/cbmc/proofs/TCP/prvSendData/SendData_harness.c
+++ b/test/cbmc/proofs/TCP/prvSendData/SendData_harness.c
@@ -36,7 +36,7 @@
 #include "FreeRTOS_TCP_IP.h"
 
 /* CBMC includes. */
-#include "../../utility/memory_assignments.c"
+#include "cbmc.h"
 
 /****************************************************************
 * Declare the IP Header Size external to the harness so it can be
@@ -52,15 +52,73 @@ size_t uxIPHeaderSizePacket( const NetworkBufferDescriptor_t * pxNetworkBuffer )
     return uxIPHeaderSizePacket_uxResult;
 }
 
+void prvTCPReturnPacket( FreeRTOS_Socket_t * pxSocket,
+                         NetworkBufferDescriptor_t * pxDescriptor,
+                         uint32_t ulLen,
+                         BaseType_t xReleaseAfterSend )
+{
+    __CPROVER_assert( pxSocket != NULL, "pxSocket should not be NULL" );
+    __CPROVER_assert( pxDescriptor != NULL, "pxDescriptor should not be NULL" );
+    __CPROVER_assert( pxDescriptor->pucEthernetBuffer != NULL, "pucEthernetBuffer should not be NULL" );
+}
+
+void prvTCPReturnPacket_IPV4( FreeRTOS_Socket_t * pxSocket,
+                              NetworkBufferDescriptor_t * pxDescriptor,
+                              uint32_t ulLen,
+                              BaseType_t xReleaseAfterSend )
+{
+    __CPROVER_assert( pxSocket != NULL, "pxSocket should not be NULL" );
+    __CPROVER_assert( pxDescriptor != NULL, "pxDescriptor should not be NULL" );
+    __CPROVER_assert( pxDescriptor->pucEthernetBuffer != NULL, "pucEthernetBuffer should not be NULL" );
+}
+
+/* Memory assignment for FreeRTOS_Socket_t */
+FreeRTOS_Socket_t * ensure_FreeRTOS_Socket_t_is_allocated()
+{
+    size_t buf_size; /* Give buffer_size an unconstrained value */
+    FreeRTOS_Socket_t * pxSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) );
+
+    __CPROVER_assume( pxSocket != NULL );
+    pxSocket->u.xTCP.rxStream = safeMalloc( sizeof( StreamBuffer_t ) );
+    pxSocket->u.xTCP.txStream = safeMalloc( sizeof( StreamBuffer_t ) );
+    pxSocket->u.xTCP.pxPeerSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) );
+    pxSocket->pxEndPoint = safeMalloc( sizeof( NetworkEndPoint_t ) );
+    pxSocket->u.xTCP.pxAckMessage = safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
+    if( pxSocket->u.xTCP.pxAckMessage != NULL )
+    {
+        __CPROVER_assume( ( buf_size > ( ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + sizeof( TCPHeader_t ) ) ) && ( buf_size < ipconfigNETWORK_MTU ) );
+        pxSocket->u.xTCP.pxAckMessage->pucEthernetBuffer = safeMalloc( buf_size );
+        __CPROVER_assume( pxSocket->u.xTCP.pxAckMessage->pucEthernetBuffer != NULL );
+    }
+
+    return pxSocket;
+}
+
+/* 
+ * In this function, it only allocates network buffer by harness.
+ */
+void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer )
+{
+    __CPROVER_assert( pxNetworkBuffer != NULL,
+                      "Precondition: pxNetworkBuffer != NULL" );
+
+    if( pxNetworkBuffer->pucEthernetBuffer != NULL )
+    {
+        free( pxNetworkBuffer->pucEthernetBuffer );
+    }
+    free( pxNetworkBuffer );
+}
+
 void harness()
 {
     FreeRTOS_Socket_t * pxSocket = ensure_FreeRTOS_Socket_t_is_allocated();
-    NetworkBufferDescriptor_t * pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated();
+    NetworkBufferDescriptor_t * pxNetworkBuffer;
     uint32_t ulReceiveLength;
     BaseType_t xByteCount;
     size_t buf_size; /* Give buffer_size an unconstrained value */
 
     /* The code does not expect pxSocket/pxNetworkBuffer to be equal to NULL. */
+    pxNetworkBuffer = safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
     __CPROVER_assume( pxSocket != NULL );
     __CPROVER_assume( pxNetworkBuffer != NULL );
 
@@ -73,7 +131,7 @@ void harness()
         uxIPHeaderSizePacket_uxResult = ipSIZE_OF_IPv4_HEADER;
     }
 
-    __CPROVER_assume( buf_size > ( ipSIZE_OF_ETH_HEADER + uxIPHeaderSizePacket_uxResult + sizeof( TCPHeader_t ) ) );
+    __CPROVER_assume( ( buf_size > ( ipSIZE_OF_ETH_HEADER + uxIPHeaderSizePacket_uxResult + sizeof( TCPHeader_t ) ) ) && ( buf_size < ipconfigNETWORK_MTU ) );
 
     pxNetworkBuffer->pucEthernetBuffer = safeMalloc( buf_size );
     __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
diff --git a/test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json b/test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json
index c82fbddc3..bc6f29b9c 100644
--- a/test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json
+++ b/test/cbmc/proofs/TCP/prvTCPHandleState/Makefile.json
@@ -45,18 +45,21 @@
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Reception.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto"
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto"
   ],
   "DEF":
   [
+    "ipconfigUSE_TCP=1",
     "ipconfigZERO_COPY_TX_DRIVER={TX_DRIVER}",
     "ipconfigUSE_LINKED_RX_MESSAGES={RX_MESSAGES}",
-    "FREERTOS_TCP_ENABLE_VERIFICATION"
+    "FREERTOS_TCP_ENABLE_VERIFICATION",
+    "ipconfigNETWORK_MTU=586"
   ],
   "INSTFLAGS":
   [
-    "--remove-function-body prvTCPPrepareSend",
-    "--remove-function-body prvTCPReturnPacket"
   ],
   "INC":
   [
diff --git a/test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c b/test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c
index 1f5f99ea6..8107322b3 100644
--- a/test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c
+++ b/test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c
@@ -35,7 +35,8 @@
 #include "FreeRTOS_IP_Private.h"
 #include "FreeRTOS_TCP_IP.h"
 
-#include "../../utility/memory_assignments.c"
+/* CBMC includes. */
+#include "cbmc.h"
 
 extern FreeRTOS_Socket_t * xSocketToListen;
 
@@ -61,32 +62,207 @@ TaskHandle_t xTaskGetCurrentTaskHandle( void )
 BaseType_t publicTCPHandleState( FreeRTOS_Socket_t * pxSocket,
                                  NetworkBufferDescriptor_t ** ppxNetworkBuffer );
 
+void * vSocketClose( FreeRTOS_Socket_t * pxSocket )
+{
+    __CPROVER_assert( pxSocket != NULL, "Closing socket cannot be NULL." );
+
+    return NULL;
+}
+
+void vSocketWakeUpUser( FreeRTOS_Socket_t * pxSocket )
+{
+    __CPROVER_assert( pxSocket != NULL, "Closing socket cannot be NULL." );
+
+    return NULL;
+}
+
+/* Memory assignment for FreeRTOS_Socket_t */
+FreeRTOS_Socket_t * ensure_FreeRTOS_Socket_t_is_allocated()
+{
+    size_t buf_size; /* Give buffer_size an unconstrained value */
+    FreeRTOS_Socket_t * pxSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) );
+
+    __CPROVER_assume( pxSocket != NULL );
+    pxSocket->u.xTCP.rxStream = safeMalloc( sizeof( StreamBuffer_t ) );
+    pxSocket->u.xTCP.txStream = safeMalloc( sizeof( StreamBuffer_t ) );
+    pxSocket->u.xTCP.pxPeerSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) );
+    pxSocket->pxEndPoint = safeMalloc( sizeof( NetworkEndPoint_t ) );
+    pxSocket->u.xTCP.pxAckMessage = safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
+    if( pxSocket->u.xTCP.pxAckMessage != NULL )
+    {
+        __CPROVER_assume( ( buf_size > ( ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + sizeof( TCPHeader_t ) ) ) && ( buf_size < ipconfigNETWORK_MTU ) );
+        pxSocket->u.xTCP.pxAckMessage->pucEthernetBuffer = safeMalloc( buf_size );
+        __CPROVER_assume( pxSocket->u.xTCP.pxAckMessage->pucEthernetBuffer != NULL );
+    }
+
+    return pxSocket;
+}
+
+/* lTCPAddRxdata is proven separately. */
+int32_t lTCPAddRxdata( FreeRTOS_Socket_t * pxSocket,
+                       size_t uxOffset,
+                       const uint8_t * pcData,
+                       uint32_t ulByteCount )
+{
+    return nondet_int32();
+}
+
+/* prvSendData is proven separately. */
+BaseType_t prvSendData( FreeRTOS_Socket_t * pxSocket,
+                        NetworkBufferDescriptor_t ** ppxNetworkBuffer,
+                        uint32_t ulReceiveLength,
+                        BaseType_t xByteCount )
+{
+    __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" );
+    __CPROVER_assert( *ppxNetworkBuffer != NULL, "*ppxNetworkBuffer cannot be NULL" );
+
+    return nondet_BaseType();
+}
+
+/* prvTCPPrepareSend is proven separately. */
+int32_t prvTCPPrepareSend( FreeRTOS_Socket_t * pxSocket,
+                           NetworkBufferDescriptor_t ** ppxNetworkBuffer,
+                           UBaseType_t uxOptionsLength )
+{
+    __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" );
+    __CPROVER_assert( *ppxNetworkBuffer != NULL, "*ppxNetworkBuffer cannot be NULL" );
+
+    return nondet_int32();
+}
+
+/* Mock all window APIs */
+int32_t lTCPWindowRxCheck( TCPWindow_t * pxWindow,
+                           uint32_t ulSequenceNumber,
+                           uint32_t ulLength,
+                           uint32_t ulSpace,
+                           uint32_t * pulSkipCount )
+{
+    __CPROVER_assert( pxWindow != NULL, "pxWindow cannot be NULL" );
+    __CPROVER_assert( __CPROVER_r_ok( pxWindow, sizeof( TCPWindow_t ) ), "pxWindow must be readable" );
+    *pulSkipCount = nondet_uint32();
+    
+    return nondet_int32();
+}
+
+uint32_t ulTCPWindowTxAck( TCPWindow_t * pxWindow,
+                           uint32_t ulSequenceNumber )
+{
+    __CPROVER_assert( pxWindow != NULL, "pxWindow cannot be NULL" );
+    __CPROVER_assert( __CPROVER_r_ok( pxWindow, sizeof( TCPWindow_t ) ), "pxWindow must be readable" );
+
+    return nondet_uint32();
+}
+
+void vTCPWindowInit( TCPWindow_t * pxWindow,
+                     uint32_t ulAckNumber,
+                     uint32_t ulSequenceNumber,
+                     uint32_t ulMSS )
+{
+    __CPROVER_assert( pxWindow != NULL, "pxWindow cannot be NULL" );
+    __CPROVER_assert( __CPROVER_r_ok( pxWindow, sizeof( TCPWindow_t ) ), "pxWindow must be readable" );
+}
+
+BaseType_t xTCPWindowRxEmpty( const TCPWindow_t * pxWindow )
+{
+    __CPROVER_assert( pxWindow != NULL, "pxWindow cannot be NULL" );
+    __CPROVER_assert( __CPROVER_r_ok( pxWindow, sizeof( TCPWindow_t ) ), "pxWindow must be readable" );
+
+    return nondet_BaseType();
+}
+
+BaseType_t xTCPWindowTxDone( const TCPWindow_t * pxWindow )
+{
+    __CPROVER_assert( pxWindow != NULL, "pxWindow cannot be NULL" );
+    __CPROVER_assert( __CPROVER_r_ok( pxWindow, sizeof( TCPWindow_t ) ), "pxWindow must be readable" );
+
+    return nondet_BaseType();
+}
+
+/* Mock all stream buffer APIs */
+size_t uxStreamBufferGet( StreamBuffer_t * const pxBuffer,
+                          size_t uxOffset,
+                          uint8_t * const pucData,
+                          size_t uxMaxCount,
+                          BaseType_t xPeek )
+{
+    __CPROVER_assert( pxBuffer != NULL, "pxBuffer cannot be NULL" );
+
+    return nondet_sizet();
+}
+
+size_t uxStreamBufferGetSpace( const StreamBuffer_t * const pxBuffer )
+{
+    __CPROVER_assert( pxBuffer != NULL, "pxBuffer cannot be NULL" );
+
+    return nondet_sizet();
+}
+
+/* Mock all transmission APIs. */
+UBaseType_t prvSetOptions( FreeRTOS_Socket_t * pxSocket,
+                           const NetworkBufferDescriptor_t * pxNetworkBuffer )
+{
+    __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" );
+    __CPROVER_assert( pxNetworkBuffer != NULL, "pxNetworkBuffer cannot be NULL" );
+
+    return nondet_ubasetype();
+}
+
+UBaseType_t prvSetSynAckOptions( FreeRTOS_Socket_t * pxSocket,
+                                 TCPHeader_t * pxTCPHeader )
+{
+    __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" );
+    __CPROVER_assert( pxTCPHeader != NULL, "pxTCPHeader cannot be NULL" );
+
+    return nondet_ubasetype();
+}
+
+void prvTCPAddTxData( FreeRTOS_Socket_t * pxSocket )
+{
+    __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" );
+}
+
+BaseType_t prvTCPSendReset( NetworkBufferDescriptor_t * pxNetworkBuffer )
+{
+    __CPROVER_assert( pxNetworkBuffer != NULL, "pxNetworkBuffer cannot be NULL" );
+
+    return nondet_BaseType();
+}
+
+const char * FreeRTOS_inet_ntop( BaseType_t xAddressFamily,
+                                 const void * pvSource,
+                                 char * pcDestination,
+                                 socklen_t uxSize )
+{
+    __CPROVER_assert( __CPROVER_r_ok( pcDestination, uxSize ), "input buffer must be available" );
+
+    __CPROVER_assert( ( xAddressFamily == FREERTOS_AF_INET6 && __CPROVER_r_ok( pvSource, 16 ) ) ||
+                      ( xAddressFamily == FREERTOS_AF_INET && __CPROVER_r_ok( pvSource, 4 ) ),
+                      "input address must be available" );
+}
+
 void harness()
 {
     FreeRTOS_Socket_t * pxSocket = ensure_FreeRTOS_Socket_t_is_allocated();
-    size_t socketSize = sizeof( FreeRTOS_Socket_t );
 
-    if( ensure_memory_is_valid( pxSocket, socketSize ) )
+    __CPROVER_assume( pxSocket != NULL );
+    /* ucOptionLength is the number of valid bytes in ulOptionsData[].
+     * ulOptionsData[] is initialized as uint32_t ulOptionsData[ipSIZE_TCP_OPTIONS/sizeof(uint32_t)].
+     * This assumption is required for a memcpy function that copies uxOptionsLength
+     * data from pxTCPHeader->ucOptdata to pxTCPWindow->ulOptionsData.*/
+    __CPROVER_assume( pxSocket->u.xTCP.xTCPWindow.ucOptionLength == sizeof( uint32_t ) * ipSIZE_TCP_OPTIONS / sizeof( uint32_t ) );
+    /* uxRxWinSize is initialized as size_t. This assumption is required to terminate `while(uxWinSize > 0xfffful)` loop.*/
+    __CPROVER_assume( pxSocket->u.xTCP.uxRxWinSize >= 0 && pxSocket->u.xTCP.uxRxWinSize <= sizeof( size_t ) );
+    /* uxRxWinSize is initialized as uint16_t. This assumption is required to terminate `while(uxWinSize > 0xfffful)` loop.*/
+    __CPROVER_assume( pxSocket->u.xTCP.usMSS == sizeof( uint16_t ) );
+
+    if( xIsCallingFromIPTask() == pdFALSE )
     {
-        /* ucOptionLength is the number of valid bytes in ulOptionsData[].
-         * ulOptionsData[] is initialized as uint32_t ulOptionsData[ipSIZE_TCP_OPTIONS/sizeof(uint32_t)].
-         * This assumption is required for a memcpy function that copies uxOptionsLength
-         * data from pxTCPHeader->ucOptdata to pxTCPWindow->ulOptionsData.*/
-        __CPROVER_assume( pxSocket->u.xTCP.xTCPWindow.ucOptionLength == sizeof( uint32_t ) * ipSIZE_TCP_OPTIONS / sizeof( uint32_t ) );
-        /* uxRxWinSize is initialized as size_t. This assumption is required to terminate `while(uxWinSize > 0xfffful)` loop.*/
-        __CPROVER_assume( pxSocket->u.xTCP.uxRxWinSize >= 0 && pxSocket->u.xTCP.uxRxWinSize <= sizeof( size_t ) );
-        /* uxRxWinSize is initialized as uint16_t. This assumption is required to terminate `while(uxWinSize > 0xfffful)` loop.*/
-        __CPROVER_assume( pxSocket->u.xTCP.usMSS == sizeof( uint16_t ) );
-
-        if( xIsCallingFromIPTask() == pdFALSE )
-        {
-            __CPROVER_assume( pxSocket->u.xTCP.bits.bPassQueued == pdFALSE_UNSIGNED );
-            __CPROVER_assume( pxSocket->u.xTCP.bits.bPassAccept == pdFALSE_UNSIGNED );
-        }
+        __CPROVER_assume( pxSocket->u.xTCP.bits.bPassQueued == pdFALSE_UNSIGNED );
+        __CPROVER_assume( pxSocket->u.xTCP.bits.bPassAccept == pdFALSE_UNSIGNED );
     }
 
-    NetworkBufferDescriptor_t * pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated();
-    size_t bufferSize = sizeof( NetworkBufferDescriptor_t );
+    NetworkBufferDescriptor_t * pxNetworkBuffer = safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
+    __CPROVER_assume( pxNetworkBuffer != NULL );
 
     FreeRTOS_Socket_t xSck;
     xSocketToListen = &xSck;
@@ -94,17 +270,15 @@ void harness()
     /* Call to init the socket list. */
     vListInitialise( &xBoundTCPSocketsList );
 
-    if( ensure_memory_is_valid( pxNetworkBuffer, bufferSize ) )
-    {
-        /* Allocates min. buffer size required for the proof */
-        pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( TCPPacket_t ) + uxIPHeaderSizeSocket( pxSocket ) );
-    }
+    /* Allocates min. buffer size required for the proof */
+    pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( TCPPacket_t ) + uxIPHeaderSizeSocket( pxSocket ) );
+    __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
 
-    if( ensure_memory_is_valid( pxSocket, socketSize ) &&
-        ensure_memory_is_valid( pxNetworkBuffer, bufferSize ) &&
-        ensure_memory_is_valid( pxNetworkBuffer->pucEthernetBuffer, sizeof( TCPPacket_t ) ) &&
-        ensure_memory_is_valid( pxSocket->u.xTCP.pxPeerSocket, socketSize ) )
+    if( pxSocket->u.xTCP.bits.bReuseSocket == pdFALSE )
     {
-        publicTCPHandleState( pxSocket, &pxNetworkBuffer );
+        /* Make sure we have parent socket if reuse is set to FALSE to avoid assertion in vTCPStateChange(). */
+        __CPROVER_assume( pxSocket->u.xTCP.pxPeerSocket != NULL );
     }
+
+    publicTCPHandleState( pxSocket, &pxNetworkBuffer );
 }
diff --git a/test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json b/test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json
index df1df0a68..e1dd2fdf0 100644
--- a/test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json
+++ b/test/cbmc/proofs/TCP/prvTCPPrepareSend/Makefile.json
@@ -40,7 +40,10 @@
     "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_IP.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto"
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto"
   ],
   "OPT":
   [
@@ -48,7 +51,8 @@
   ],
   "DEF":
   [
-    "FREERTOS_TCP_ENABLE_VERIFICATION"
+    "FREERTOS_TCP_ENABLE_VERIFICATION",
+    "CBMC_REQUIRE_NETWORKBUFFER_ETHERNETBUFFER_NONNULL"
   ],
   "INC":
   [
diff --git a/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c b/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c
index d889e1638..6a84f09e0 100644
--- a/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c
+++ b/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c
@@ -36,30 +36,34 @@
 #include "FreeRTOS_TCP_IP.h"
 #include "FreeRTOS_Stream_Buffer.h"
 
-#include "../../utility/memory_assignments.c"
+/* CBMC includes. */
+#include "cbmc.h"
 
 /* This proof assumes that pxGetNetworkBufferWithDescriptor is implemented correctly. */
 int32_t publicTCPPrepareSend( FreeRTOS_Socket_t * pxSocket,
                               NetworkBufferDescriptor_t ** ppxNetworkBuffer,
                               UBaseType_t uxOptionsLength );
 
-/* Abstraction of pxGetNetworkBufferWithDescriptor. It creates a buffer. */
-NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes,
-                                                              TickType_t xBlockTimeTicks )
+/* Memory assignment for FreeRTOS_Socket_t */
+FreeRTOS_Socket_t * ensure_FreeRTOS_Socket_t_is_allocated()
 {
-    NetworkBufferDescriptor_t * pxBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated();
-    size_t bufferSize = sizeof( NetworkBufferDescriptor_t );
+    size_t buf_size; /* Give buffer_size an unconstrained value */
+    FreeRTOS_Socket_t * pxSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) + sizeof( IPTCPSocket_t ) );
 
-    if( ensure_memory_is_valid( pxBuffer, bufferSize ) )
+    __CPROVER_assume( pxSocket != NULL );
+    pxSocket->u.xTCP.rxStream = safeMalloc( sizeof( StreamBuffer_t ) );
+    pxSocket->u.xTCP.txStream = safeMalloc( sizeof( StreamBuffer_t ) );
+    pxSocket->u.xTCP.pxPeerSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) );
+    pxSocket->pxEndPoint = safeMalloc( sizeof( NetworkEndPoint_t ) );
+    pxSocket->u.xTCP.pxAckMessage = safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
+    if( pxSocket->u.xTCP.pxAckMessage != NULL )
     {
-        /* The code does not expect pucEthernetBuffer to be equal to NULL if
-         * pxBuffer is not NULL. */
-        pxBuffer->pucEthernetBuffer = malloc( xRequestedSizeBytes );
-        __CPROVER_assume( pxBuffer->pucEthernetBuffer != NULL );
-        pxBuffer->xDataLength = xRequestedSizeBytes;
+        __CPROVER_assume( ( buf_size > ( ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + sizeof( TCPHeader_t ) ) ) && ( buf_size < ipconfigNETWORK_MTU ) );
+        pxSocket->u.xTCP.pxAckMessage->pucEthernetBuffer = safeMalloc( buf_size );
+        __CPROVER_assume( pxSocket->u.xTCP.pxAckMessage->pucEthernetBuffer != NULL );
     }
 
-    return pxBuffer;
+    return pxSocket;
 }
 
 /* Get rid of configASSERT in FreeRTOS_TCP_IP.c */
@@ -68,37 +72,93 @@ BaseType_t xIsCallingFromIPTask( void )
     return pdTRUE;
 }
 
-void harness()
+/* Mock FreeRTOS_TCP_State_Handling.h APIs */
+BaseType_t prvTCPSocketIsActive( eIPTCPState_t eStatus )
 {
-    FreeRTOS_Socket_t * pxSocket = malloc( sizeof( FreeRTOS_Socket_t ) );
+    return nondet_BaseType();
+}
 
-    __CPROVER_assume( pxSocket != NULL );
-    pxSocket->u.xTCP.rxStream = malloc( sizeof( StreamBuffer_t ) );
-    pxSocket->u.xTCP.txStream = malloc( sizeof( StreamBuffer_t ) );
-    pxSocket->u.xTCP.pxPeerSocket = malloc( sizeof( FreeRTOS_Socket_t ) );
+/* Mock FreeRTOS_TCP_WIN.h APIs */
+BaseType_t xTCPWindowTxDone( const TCPWindow_t * pxWindow )
+{
+    __CPROVER_assert( pxWindow != NULL, "pxWindow cannot be NULL" );
+    return nondet_uint32();
+}
+
+uint32_t ulTCPWindowTxGet( TCPWindow_t * pxWindow,
+                           uint32_t ulWindowSize,
+                           int32_t * plPosition )
+{
+    uint32_t ulReturn = nondet_uint32();
+    __CPROVER_assert( pxWindow != NULL, "pxWindow cannot be NULL" );
+    __CPROVER_assert( plPosition != NULL, "plPosition cannot be NULL" );
+
+    /* This function returns the data length of next sending window, which is never larger than network MTU. */
+    __CPROVER_assume( ulReturn < ipconfigNETWORK_MTU );
+    return ulReturn;
+}
+
+/* Mock FreeRTOS_Stream_Buffers.h APIs */
+size_t uxStreamBufferDistance( const StreamBuffer_t * const pxBuffer,
+                               size_t uxLower,
+                               size_t uxUpper )
+{
+    __CPROVER_assert( pxBuffer != NULL, "pxBuffer cannot be NULL" );
+    return nondet_sizet();
+}
+
+size_t uxStreamBufferGet( StreamBuffer_t * const pxBuffer,
+                          size_t uxOffset,
+                          uint8_t * const pucData,
+                          size_t uxMaxCount,
+                          BaseType_t xPeek )
+{
+    __CPROVER_assert( pxBuffer != NULL, "pxBuffer cannot be NULL" );
+    return nondet_sizet();
+}
+
+void * vSocketClose( FreeRTOS_Socket_t * pxSocket )
+{
+    __CPROVER_assert( pxSocket != NULL, "Closing socket cannot be NULL." );
+
+    return NULL;
+}
+
+void vSocketWakeUpUser( FreeRTOS_Socket_t * pxSocket )
+{
+    __CPROVER_assert( pxSocket != NULL, "Closing socket cannot be NULL." );
 
-    NetworkBufferDescriptor_t * pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated();
+    return NULL;
+}
+
+void harness()
+{
+    NetworkBufferDescriptor_t * pxNetworkBuffer;
+    FreeRTOS_Socket_t * pxSocket;
     size_t socketSize = sizeof( FreeRTOS_Socket_t );
     /* Allocates min. buffer size required for the proof */
-    size_t bufferSize = sizeof( TCPPacket_t ) + uxIPHeaderSizeSocket( pxSocket );
+    size_t bufferSize;
 
-    if( ensure_memory_is_valid( pxNetworkBuffer, sizeof( *pxNetworkBuffer ) ) )
-    {
-        pxNetworkBuffer->xDataLength = bufferSize;
+    pxSocket = ensure_FreeRTOS_Socket_t_is_allocated();
+    __CPROVER_assume( pxSocket != NULL );
 
-        /* The code does not expect pucEthernetBuffer to be equal to NULL if
-         * pxNetworkBuffer is not NULL. */
-        pxNetworkBuffer->pucEthernetBuffer = malloc( bufferSize );
-        __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
+    if( pxSocket->u.xTCP.bits.bReuseSocket == pdFALSE )
+    {
+        /* Make sure we have parent socket if reuse is set to FALSE to avoid assertion in vTCPStateChange(). */
+        __CPROVER_assume( pxSocket->u.xTCP.pxPeerSocket != NULL );
     }
 
-    UBaseType_t uxOptionsLength;
+    bufferSize = sizeof( TCPPacket_t ) + ipSIZE_OF_IPv6_HEADER;
+
+    pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( bufferSize, 0 );
+    __CPROVER_assume( pxNetworkBuffer != NULL );
+    __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
 
     /* Call to init the socket list. */
     vListInitialise( &xBoundTCPSocketsList );
 
     if( pxSocket )
     {
-        publicTCPPrepareSend( pxSocket, &pxNetworkBuffer, uxOptionsLength );
+        publicTCPPrepareSend( pxSocket, &pxNetworkBuffer, 0 );
     }
 }
diff --git a/test/cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json b/test/cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json
index 1b67f5a07..12a17ef30 100644
--- a/test/cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json
+++ b/test/cbmc/proofs/TCP/prvTCPReturnPacket/Makefile.json
@@ -39,14 +39,19 @@
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Stream_Buffer.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_IP.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission_IPv4.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto"
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto"
   ],
   "DEF":
   [
     "ipconfigUSE_LINKED_RX_MESSAGES={RX_MESSAGES}",
-    "FREERTOS_TCP_ENABLE_VERIFICATION"
+    "FREERTOS_TCP_ENABLE_VERIFICATION",
+    "CBMC_REQUIRE_NETWORKBUFFER_ETHERNETBUFFER_NONNULL"
   ],
   "INC":
   [
diff --git a/test/cbmc/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c b/test/cbmc/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c
index 786d10cfd..6bed552f2 100644
--- a/test/cbmc/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c
+++ b/test/cbmc/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c
@@ -37,10 +37,41 @@
 #include "FreeRTOS_TCP_IP.h"
 #include "FreeRTOS_TCP_Transmission.h"
 
-#include "../../utility/memory_assignments.c"
-
+/* CBMC includes */
 #include "cbmc.h"
 
+/* prvTCPReturnPacket_IPV6 is proven separately. */
+void prvTCPReturnPacket_IPV6( FreeRTOS_Socket_t * pxSocket,
+                              NetworkBufferDescriptor_t * pxDescriptor,
+                              uint32_t ulLen,
+                              BaseType_t xReleaseAfterSend )
+{
+    __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" );
+    __CPROVER_assert( pxDescriptor != NULL, "pxDescriptor cannot be NULL" );
+}
+
+/* Memory assignment for FreeRTOS_Socket_t */
+FreeRTOS_Socket_t * ensure_FreeRTOS_Socket_t_is_allocated()
+{
+    size_t buf_size; /* Give buffer_size an unconstrained value */
+    FreeRTOS_Socket_t * pxSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) + sizeof( IPTCPSocket_t ) );
+
+    __CPROVER_assume( pxSocket != NULL );
+    pxSocket->u.xTCP.rxStream = safeMalloc( sizeof( StreamBuffer_t ) );
+    pxSocket->u.xTCP.txStream = safeMalloc( sizeof( StreamBuffer_t ) );
+    pxSocket->u.xTCP.pxPeerSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) );
+    pxSocket->pxEndPoint = safeMalloc( sizeof( NetworkEndPoint_t ) );
+    pxSocket->u.xTCP.pxAckMessage = safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
+    if( pxSocket->u.xTCP.pxAckMessage != NULL )
+    {
+        __CPROVER_assume( ( buf_size > ( ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + sizeof( TCPHeader_t ) ) ) && ( buf_size < ipconfigNETWORK_MTU ) );
+        pxSocket->u.xTCP.pxAckMessage->pucEthernetBuffer = safeMalloc( buf_size );
+        __CPROVER_assume( pxSocket->u.xTCP.pxAckMessage->pucEthernetBuffer != NULL );
+    }
+
+    return pxSocket;
+}
+
 /*
  * This function is implemented by a third party.
  * After looking through a couple of samples in the demos folder, it seems
@@ -89,27 +120,31 @@ void prvTCPReturn_SetEndPoint( const FreeRTOS_Socket_t * pxSocket,
 NetworkBufferDescriptor_t * pxDuplicateNetworkBufferWithDescriptor( const NetworkBufferDescriptor_t * const pxNetworkBuffer,
                                                                     size_t xNewLength )
 {
-    NetworkBufferDescriptor_t * pxNetworkBuffer = safeMalloc( xNewLength );
+    NetworkBufferDescriptor_t * pxLocalNetworkBuffer;
+    EthernetHeader_t * pxHeader;
+
+    pxLocalNetworkBuffer = pxGetNetworkBufferWithDescriptor( xNewLength, 0 );
 
-    if( ensure_memory_is_valid( pxNetworkBuffer, xNewLength ) )
+    if( pxLocalNetworkBuffer != NULL )
     {
-        pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( TCPPacket_t ) );
-        __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer );
+        /* In this test case, we only focus on IPv4. */
+        pxHeader = ( ( const EthernetHeader_t * ) pxNetworkBuffer->pucEthernetBuffer );
+        __CPROVER_assume( pxHeader->usFrameType != ipIPv6_FRAME_TYPE );
 
         /* 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 * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
-        __CPROVER_assume( pxNetworkBuffer->pxEndPoint != NULL );
-        pxNetworkBuffer->pxEndPoint->pxNext = NULL;
+        pxLocalNetworkBuffer->pxEndPoint = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
+        __CPROVER_assume( pxLocalNetworkBuffer->pxEndPoint != NULL );
+        pxLocalNetworkBuffer->pxEndPoint->pxNext = NULL;
 
         /* Add an interface */
-        pxNetworkBuffer->pxEndPoint->pxNetworkInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) );
-        __CPROVER_assume( pxNetworkBuffer->pxEndPoint->pxNetworkInterface != NULL );
+        pxLocalNetworkBuffer->pxEndPoint->pxNetworkInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) );
+        __CPROVER_assume( pxLocalNetworkBuffer->pxEndPoint->pxNetworkInterface != NULL );
 
-        pxNetworkBuffer->pxEndPoint->pxNetworkInterface->pfOutput = NetworkInterfaceOutputFunction_Stub;
+        pxLocalNetworkBuffer->pxEndPoint->pxNetworkInterface->pfOutput = NetworkInterfaceOutputFunction_Stub;
     }
 
-    return pxNetworkBuffer;
+    return pxLocalNetworkBuffer;
 }
 
 uint16_t usGenerateProtocolChecksum( const uint8_t * const pucEthernetBuffer,
@@ -169,29 +204,43 @@ eARPLookupResult_t eARPGetCacheEntry( uint32_t * pulIPAddress,
 
 void harness()
 {
-    FreeRTOS_Socket_t * pxSocket = ensure_FreeRTOS_Socket_t_is_allocated();
-    NetworkBufferDescriptor_t * pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated();
+    FreeRTOS_Socket_t * pxSocket;
+    NetworkBufferDescriptor_t * pxNetworkBuffer;
     BaseType_t xReleaseAfterSend;
     uint32_t ulLen;
+    EthernetHeader_t * pxHeader;
+
+    pxSocket = ensure_FreeRTOS_Socket_t_is_allocated();
+    if( pxSocket != NULL )
+    {
+        /* In this test case, we only focus on IPv4. */
+        __CPROVER_assume( pxSocket->bits.bIsIPv6 == pdFALSE_UNSIGNED );
+    }
+
+    // if( pxSocket->u.xTCP.bits.bReuseSocket == pdFALSE )
+    // {
+    //     /* Make sure we have parent socket if reuse is set to FALSE to avoid assertion in vTCPStateChange(). */
+    //     __CPROVER_assume( pxSocket->u.xTCP.pxPeerSocket != NULL );
+    // }
+
+    __CPROVER_assume( ( ulLen >= sizeof( TCPPacket_t ) ) && ( ulLen < ipconfigNETWORK_MTU - ipSIZE_OF_ETH_HEADER ) );
+    pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( ulLen + ipSIZE_OF_ETH_HEADER, 0 );
 
     /* The code does not expect both of these to be equal to NULL at the same time. */
     __CPROVER_assume( pxSocket != NULL || pxNetworkBuffer != NULL );
 
     /* If network buffer is properly created. */
-    if( ensure_memory_is_valid( pxNetworkBuffer, sizeof( *pxNetworkBuffer ) ) )
+    if( pxNetworkBuffer != NULL )
     {
-        /* Assume that the length is proper. */
-        __CPROVER_assume( ( ulLen >= sizeof( TCPPacket_t ) ) && ( ulLen < ipconfigNETWORK_MTU ) );
-        pxNetworkBuffer->pucEthernetBuffer = safeMalloc( ulLen + ipSIZE_OF_ETH_HEADER );
-        __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer );
-
-        pxNetworkBuffer->xDataLength = ( size_t ) ulLen;
+        /* In this test case, we only focus on IPv4. */
+        pxHeader = ( ( const EthernetHeader_t * ) pxNetworkBuffer->pucEthernetBuffer );
+        __CPROVER_assume( pxHeader->usFrameType != ipIPv6_FRAME_TYPE );
 
         /* 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 * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
 
-        if( ensure_memory_is_valid( pxNetworkBuffer->pxEndPoint, sizeof( NetworkEndPoint_t ) ) )
+        if( pxNetworkBuffer->pxEndPoint != NULL )
         {
             /* Add an interface */
             pxNetworkBuffer->pxEndPoint->pxNetworkInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) );
diff --git a/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/Makefile.json b/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/Makefile.json
index 9b28c3b34..629ef713d 100644
--- a/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/Makefile.json
+++ b/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/Makefile.json
@@ -11,14 +11,19 @@
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Stream_Buffer.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_IP.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission_IPv6.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto"
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto"
   ],
   "DEF":
   [
     "ipconfigUSE_LINKED_RX_MESSAGES={RX_MESSAGES}",
-    "FREERTOS_TCP_ENABLE_VERIFICATION"
+    "FREERTOS_TCP_ENABLE_VERIFICATION",
+    "CBMC_REQUIRE_NETWORKBUFFER_ETHERNETBUFFER_NONNULL"
   ],
   "INC":
   [
diff --git a/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/TCPReturnPacket_IPv6_harness.c b/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/TCPReturnPacket_IPv6_harness.c
index ea2e87b2f..b029febce 100644
--- a/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/TCPReturnPacket_IPv6_harness.c
+++ b/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/TCPReturnPacket_IPv6_harness.c
@@ -35,10 +35,9 @@
 #include "FreeRTOS_IP_Private.h"
 #include "FreeRTOS_TCP_IP.h"
 #include "FreeRTOS_TCP_Transmission.h"
+#include "FreeRTOS_ND.h"
 
 /* CBMC includes. */
-#include "../../utility/memory_assignments.c"
-
 #include "cbmc.h"
 
 /*
@@ -64,6 +63,50 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes
     return 0;
 }
 
+/* Memory assignment for FreeRTOS_Socket_t */
+FreeRTOS_Socket_t * ensure_FreeRTOS_Socket_t_is_allocated()
+{
+    size_t buf_size; /* Give buffer_size an unconstrained value */
+    FreeRTOS_Socket_t * pxSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) + sizeof( IPTCPSocket_t ) );
+
+    __CPROVER_assume( pxSocket != NULL );
+    pxSocket->u.xTCP.rxStream = safeMalloc( sizeof( StreamBuffer_t ) );
+    pxSocket->u.xTCP.txStream = safeMalloc( sizeof( StreamBuffer_t ) );
+    pxSocket->u.xTCP.pxPeerSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) );
+    pxSocket->pxEndPoint = safeMalloc( sizeof( NetworkEndPoint_t ) );
+    pxSocket->u.xTCP.pxAckMessage = safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
+    if( pxSocket->u.xTCP.pxAckMessage != NULL )
+    {
+        __CPROVER_assume( ( buf_size > ( ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + sizeof( TCPHeader_t ) ) ) && ( buf_size < ipconfigNETWORK_MTU ) );
+        pxSocket->u.xTCP.pxAckMessage->pucEthernetBuffer = safeMalloc( buf_size );
+        __CPROVER_assume( pxSocket->u.xTCP.pxAckMessage->pucEthernetBuffer != NULL );
+    }
+
+    return pxSocket;
+}
+
+void prvTCPReturnPacket_IPV4( FreeRTOS_Socket_t * pxSocket,
+                              NetworkBufferDescriptor_t * pxDescriptor,
+                              uint32_t ulLen,
+                              BaseType_t xReleaseAfterSend )
+{
+    __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" );
+    __CPROVER_assert( pxDescriptor != NULL, "pxDescriptor cannot be NULL" );
+}
+
+/* Abstraction of eNDGetCacheEntry. */
+eARPLookupResult_t eNDGetCacheEntry( IPv6_Address_t * pxIPAddress,
+                                     MACAddress_t * const pxMACAddress,
+                                     struct xNetworkEndPoint ** ppxEndPoint )
+{
+    eARPLookupResult_t xReturn;
+
+    __CPROVER_assert( __CPROVER_r_ok( pxIPAddress, sizeof( IPv6_Address_t ) ), "pxIPAddress must be readable" );
+    __CPROVER_assert( __CPROVER_w_ok( pxMACAddress, sizeof( MACAddress_t ) ), "pxMACAddress must be writeable" );
+
+    return xReturn;
+}
+
 /* Abstraction of this functions creates an endpoint and assign it to network interface
  * endpoint, real endpoint doesn't matter in this test. */
 void prvTCPReturn_SetEndPoint( const FreeRTOS_Socket_t * pxSocket,
@@ -87,27 +130,31 @@ void prvTCPReturn_SetEndPoint( const FreeRTOS_Socket_t * pxSocket,
 NetworkBufferDescriptor_t * pxDuplicateNetworkBufferWithDescriptor( const NetworkBufferDescriptor_t * const pxNetworkBuffer,
                                                                     size_t xNewLength )
 {
-    NetworkBufferDescriptor_t * pxNetworkBuffer = safeMalloc( xNewLength );
+    NetworkBufferDescriptor_t * pxLocalNetworkBuffer;
+    EthernetHeader_t * pxHeader;
+
+    pxLocalNetworkBuffer = pxGetNetworkBufferWithDescriptor( xNewLength, 0 );
 
-    if( ensure_memory_is_valid( pxNetworkBuffer, xNewLength ) )
+    if( pxLocalNetworkBuffer != NULL )
     {
-        pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( TCPPacket_t ) );
-        __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer );
+        /* In this test case, we only focus on IPv6. */
+        pxHeader = ( ( const EthernetHeader_t * ) pxNetworkBuffer->pucEthernetBuffer );
+        __CPROVER_assume( pxHeader->usFrameType == ipIPv6_FRAME_TYPE );
 
         /* 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 * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
-        __CPROVER_assume( pxNetworkBuffer->pxEndPoint != NULL );
-        pxNetworkBuffer->pxEndPoint->pxNext = NULL;
+        pxLocalNetworkBuffer->pxEndPoint = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
+        __CPROVER_assume( pxLocalNetworkBuffer->pxEndPoint != NULL );
+        pxLocalNetworkBuffer->pxEndPoint->pxNext = NULL;
 
         /* Add an interface */
-        pxNetworkBuffer->pxEndPoint->pxNetworkInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) );
-        __CPROVER_assume( pxNetworkBuffer->pxEndPoint->pxNetworkInterface != NULL );
+        pxLocalNetworkBuffer->pxEndPoint->pxNetworkInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) );
+        __CPROVER_assume( pxLocalNetworkBuffer->pxEndPoint->pxNetworkInterface != NULL );
 
-        pxNetworkBuffer->pxEndPoint->pxNetworkInterface->pfOutput = NetworkInterfaceOutputFunction_Stub;
+        pxLocalNetworkBuffer->pxEndPoint->pxNetworkInterface->pfOutput = NetworkInterfaceOutputFunction_Stub;
     }
 
-    return pxNetworkBuffer;
+    return pxLocalNetworkBuffer;
 }
 
 uint16_t usGenerateProtocolChecksum( const uint8_t * const pucEthernetBuffer,
@@ -136,29 +183,37 @@ uint16_t usGenerateChecksum( uint16_t usSum,
 
 void harness()
 {
-    FreeRTOS_Socket_t * pxSocket = ensure_FreeRTOS_Socket_t_is_allocated();
-    NetworkBufferDescriptor_t * pxNetworkBuffer = ensure_FreeRTOS_NetworkBuffer_is_allocated();
+    FreeRTOS_Socket_t * pxSocket;
+    NetworkBufferDescriptor_t * pxNetworkBuffer;
     BaseType_t xReleaseAfterSend;
     uint32_t ulLen;
+    EthernetHeader_t * pxHeader;
+
+    pxSocket = ensure_FreeRTOS_Socket_t_is_allocated();
+    if( pxSocket != NULL )
+    {
+        /* In this test case, we only focus on IPv6. */
+        __CPROVER_assume( pxSocket->bits.bIsIPv6 != pdFALSE_UNSIGNED );
+    }
+
+    __CPROVER_assume( ( ulLen >= sizeof( TCPPacket_IPv6_t ) ) && ( ulLen < ipconfigNETWORK_MTU - ipSIZE_OF_ETH_HEADER ) );
+    pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( ulLen + ipSIZE_OF_ETH_HEADER, 0 );
 
     /* The code does not expect both of these to be equal to NULL at the same time. */
     __CPROVER_assume( pxSocket != NULL || pxNetworkBuffer != NULL );
 
     /* If network buffer is properly created. */
-    if( ensure_memory_is_valid( pxNetworkBuffer, sizeof( *pxNetworkBuffer ) ) )
+    if( pxNetworkBuffer != NULL )
     {
-        /* Assume that the length is proper. */
-        __CPROVER_assume( ( ulLen >= sizeof( TCPPacket_IPv6_t ) ) && ( ulLen < ipconfigNETWORK_MTU ) );
-        pxNetworkBuffer->pucEthernetBuffer = safeMalloc( ulLen + ipSIZE_OF_ETH_HEADER );
-        __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
-
-        pxNetworkBuffer->xDataLength = ( size_t ) ( ulLen + ipSIZE_OF_ETH_HEADER );
+        /* In this test case, we only focus on IPv6. */
+        pxHeader = ( ( const EthernetHeader_t * ) pxNetworkBuffer->pucEthernetBuffer );
+        __CPROVER_assume( pxHeader->usFrameType == ipIPv6_FRAME_TYPE );
 
         /* 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 * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
 
-        if( ensure_memory_is_valid( pxNetworkBuffer->pxEndPoint, sizeof( NetworkEndPoint_t ) ) )
+        if( pxNetworkBuffer->pxEndPoint != NULL )
         {
             /* Add an interface */
             pxNetworkBuffer->pxEndPoint->pxNetworkInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) );
diff --git a/test/cbmc/stubs/freertos_api.c b/test/cbmc/stubs/freertos_api.c
index 3edadc623..8d068614c 100644
--- a/test/cbmc/stubs/freertos_api.c
+++ b/test/cbmc/stubs/freertos_api.c
@@ -49,6 +49,21 @@ Socket_t FreeRTOS_socket( BaseType_t xDomain,
     }
 }
 
+/****************************************************************
+* Abstract FreeRTOS_socket.
+* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/socket.html
+*
+* We stub out this function to do nothing but allocate space for a
+* socket containing unconstrained data or return an error.
+****************************************************************/
+
+BaseType_t FreeRTOS_listen( Socket_t xSocket,
+                            BaseType_t xBacklog )
+{
+    __CPROVER_assert( xSocket != NULL, "Socket cannot be NULL" );
+    return nondet_BaseType();
+}
+
 /****************************************************************
 * Abstract FreeRTOS_setsockopt.
 * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/setsockopt.html
@@ -415,3 +430,16 @@ BaseType_t xApplicationGetRandomNumber( uint32_t * pulNumber )
 }
 
 /****************************************************************/
+
+/****************************************************************
+* Abstract vIPSetARPResolutionTimerEnableState
+****************************************************************/
+uint32_t ulApplicationGetNextSequenceNumber( uint32_t ulSourceAddress,
+                                             uint16_t usSourcePort,
+                                             uint32_t ulDestinationAddress,
+                                             uint16_t usDestinationPort )
+{
+    return nondet_uint32();
+}
+
+/****************************************************************/

From 1ff027cbf8f82dfa83c55e8492f04ecb9679b508 Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Tue, 16 Jul 2024 06:53:04 +0000
Subject: [PATCH 28/36] Fix UDP CBMC test

---
 .../vProcessGeneratedUDPPacket_harness.c                   | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c b/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c
index b56bc475b..5d8239d8a 100644
--- a/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c
+++ b/test/cbmc/proofs/UDP/vProcessGeneratedUDPPacket/vProcessGeneratedUDPPacket_harness.c
@@ -19,6 +19,12 @@
 #include "memory_assignments.c"
 #include "freertos_api.c"
 
+/* vProcessGeneratedUDPPacket_IPv6 is proven separately. */
+void vProcessGeneratedUDPPacket_IPv6( NetworkBufferDescriptor_t * const pxNetworkBuffer )
+{
+    __CPROVER_assert( pxNetworkBuffer != NULL, "pxNetworkBuffer cannot be NULL" );
+}
+
 /* We do not need to calculate the actual checksum for the proof to be complete.
  * Neither does the checksum matter for completeness. */
 uint16_t usGenerateChecksum( uint16_t usSum,
@@ -33,7 +39,6 @@ uint16_t usGenerateChecksum( uint16_t usSum,
     return usChecksum;
 }
 
-
 /* We do not need to calculate the actual checksum for the proof to be complete.
  * Neither does the checksum matter for completeness. */
 uint16_t usGenerateProtocolChecksum( const uint8_t * const pucEthernetBuffer,

From 3561b820d08345756fd781d469421902c11b9691 Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Tue, 16 Jul 2024 06:55:21 +0000
Subject: [PATCH 29/36] Fix prvChecksumIPv6Checks CBMC test

---
 test/cbmc/proofs/prvChecksumIPv6Checks/Makefile.json | 1 +
 1 file changed, 1 insertion(+)

diff --git a/test/cbmc/proofs/prvChecksumIPv6Checks/Makefile.json b/test/cbmc/proofs/prvChecksumIPv6Checks/Makefile.json
index 9645ee00a..7d84cfcee 100644
--- a/test/cbmc/proofs/prvChecksumIPv6Checks/Makefile.json
+++ b/test/cbmc/proofs/prvChecksumIPv6Checks/Makefile.json
@@ -13,6 +13,7 @@
   [
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IPv6.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IPv6_Utils.goto"
   ],
   "INSTFLAGS":

From 90a498c57bfc830dbeabb951861defc28144fcd4 Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Tue, 16 Jul 2024 08:28:47 +0000
Subject: [PATCH 30/36] Fix parsing CBMC test

---
 .../ProcessIPPacket/ProcessIPPacket_harness.c | 94 ++++++++++++++++++-
 .../ProcessReceivedTCPPacket/Makefile.json    | 11 +--
 .../ProcessReceivedTCPPacket_harness.c        | 83 +++++++++++++++-
 .../Makefile.json                             | 16 +---
 .../ProcessReceivedTCPPacket_IPv6_harness.c   | 12 +--
 .../ProcessReceivedUDPPacket/Makefile.json    |  2 +
 .../ProcessReceivedUDPPacket_harness.c        | 47 ++++------
 7 files changed, 207 insertions(+), 58 deletions(-)

diff --git a/test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c b/test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c
index a1c0c80b0..bfa47ad81 100644
--- a/test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c
+++ b/test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c
@@ -9,9 +9,97 @@
 /* CBMC includes. */
 #include "cbmc.h"
 
+NetworkEndPoint_t xEndpoint;
+
 eFrameProcessingResult_t __CPROVER_file_local_FreeRTOS_IP_c_prvProcessIPPacket( const IPPacket_t * pxIPPacket,
                                                                                 NetworkBufferDescriptor_t * const pxNetworkBuffer );
 
+/* Check if input is a valid extension header ID. */
+BaseType_t xIsExtensionHeader( uint8_t ucCurrentHeader )
+{
+    BaseType_t xReturn = pdFALSE;
+
+    switch( ucCurrentHeader )
+    {
+        case ipIPv6_EXT_HEADER_HOP_BY_HOP:
+        case ipIPv6_EXT_HEADER_DESTINATION_OPTIONS:
+        case ipIPv6_EXT_HEADER_ROUTING_HEADER:
+        case ipIPv6_EXT_HEADER_FRAGMENT_HEADER:
+        case ipIPv6_EXT_HEADER_AUTHEN_HEADER:
+        case ipIPv6_EXT_HEADER_SECURE_PAYLOAD:
+        case ipIPv6_EXT_HEADER_MOBILITY_HEADER:
+            xReturn = pdTRUE;
+            break;
+    }
+
+    return xReturn;
+}
+
+/* Abstraction of xGetExtensionOrder. To ensure the result of prepared extension headers is same. */
+BaseType_t xGetExtensionOrder( uint8_t ucProtocol,
+                               uint8_t ucNextHeader )
+{
+    return xIsExtensionHeader( ucProtocol );
+}
+
+BaseType_t xCheckRequiresARPResolution( const NetworkBufferDescriptor_t * pxNetworkBuffer )
+{
+    BaseType_t xReturn;
+    
+    __CPROVER_assert( pxNetworkBuffer != NULL, "pxNetworkBuffer cannot be NULL" );
+    __CPROVER_assert( __CPROVER_r_ok( pxNetworkBuffer->pucEthernetBuffer, pxNetworkBuffer->xDataLength ), "Data in pxNetworkBuffer must be readable" );
+}
+
+void vARPRefreshCacheEntryAge( const MACAddress_t * pxMACAddress,
+                               const uint32_t ulIPAddress )
+{
+    __CPROVER_assert( pxMACAddress != NULL, "pxMACAddress cannot be NULL" );
+}
+
+void vNDRefreshCacheEntry( const MACAddress_t * pxMACAddress,
+                           const IPv6_Address_t * pxIPAddress,
+                           NetworkEndPoint_t * pxEndPoint )
+{
+    __CPROVER_assert( pxMACAddress != NULL, "pxMACAddress cannot be NULL" );
+    __CPROVER_assert( pxIPAddress != NULL, "pxIPAddress cannot be NULL" );
+    __CPROVER_assert( pxEndPoint != NULL, "pxEndPoint cannot be NULL" );
+}
+
+NetworkEndPoint_t * FreeRTOS_FindEndPointOnIP_IPv4( uint32_t ulIPAddress,
+                                                    uint32_t ulWhere )
+{
+    NetworkEndPoint_t * pxEndpoint = NULL;
+
+    if( nondet_bool() )
+    {
+        pxEndpoint = pxNetworkEndPoints;
+    }
+
+    return pxEndpoint;
+}
+
+/* proof is done separately */
+eFrameProcessingResult_t ProcessICMPPacket( const NetworkBufferDescriptor_t * const pxNetworkBuffer )
+{
+    eFrameProcessingResult_t xReturn;
+    
+    __CPROVER_assert( pxNetworkBuffer != NULL, "pxEndPoint cannot be NULL" );
+    __CPROVER_assert( __CPROVER_r_ok( pxNetworkBuffer->pucEthernetBuffer, pxNetworkBuffer->xDataLength ), "Data in pxNetworkBuffer must be readable" );
+
+    return xReturn;
+}
+
+/* proof is done separately */
+eFrameProcessingResult_t prvProcessICMPMessage_IPv6( NetworkBufferDescriptor_t * const pxNetworkBuffer )
+{
+    eFrameProcessingResult_t xReturn;
+    
+    __CPROVER_assert( pxNetworkBuffer != NULL, "pxEndPoint cannot be NULL" );
+    __CPROVER_assert( __CPROVER_r_ok( pxNetworkBuffer->pucEthernetBuffer, pxNetworkBuffer->xDataLength ), "Data in pxNetworkBuffer must be readable" );
+
+    return xReturn;
+}
+
 /* proof is done separately */
 BaseType_t xProcessReceivedTCPPacket( NetworkBufferDescriptor_t * pxNetworkBuffer )
 {
@@ -67,6 +155,7 @@ void harness()
 {
     NetworkBufferDescriptor_t * const pxNetworkBuffer = safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
     uint8_t * pucEthernetBuffer = ( uint8_t * ) safeMalloc( ipTOTAL_ETHERNET_FRAME_SIZE + ipIP_TYPE_OFFSET );
+    EthernetHeader_t * pxHeader;
 
     __CPROVER_assume( pxNetworkBuffer != NULL );
     __CPROVER_assume( pucEthernetBuffer != NULL );
@@ -83,7 +172,10 @@ void harness()
     __CPROVER_assume( pxNetworkEndPoints != NULL );
     __CPROVER_assume( pxNetworkEndPoints->pxNext == NULL );
 
-    IPPacket_t * const pxIPPacket = ( IPPacket_t * ) pxNetworkBuffer->pucEthernetBuffer;
+    /* In this test case, we only focus on IPv4. */
+    pxHeader = ( ( const EthernetHeader_t * ) pxNetworkBuffer->pucEthernetBuffer );
+    __CPROVER_assume( pxHeader->usFrameType != ipIPv6_FRAME_TYPE );
 
+    IPPacket_t * const pxIPPacket = ( IPPacket_t * ) pxNetworkBuffer->pucEthernetBuffer;
     __CPROVER_file_local_FreeRTOS_IP_c_prvProcessIPPacket( pxIPPacket, pxNetworkBuffer );
 }
diff --git a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json
index f2643c9b9..bb142d42a 100644
--- a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json
+++ b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/Makefile.json
@@ -10,6 +10,8 @@
   [
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto",
@@ -23,16 +25,11 @@
   ],
   "INSTFLAGS":
   [
-    "--remove-function-body prvSingleStepTCPHeaderOptions",
-    "--remove-function-body prvCheckOptions",
-    "--remove-function-body prvTCPPrepareSend",
-    "--remove-function-body prvTCPReturnPacket",
-    "--remove-function-body prvTCPHandleState",
-    "--remove-function-body vTCPStateChange"
   ],
   "DEF":
   [
-    "FREERTOS_TCP_ENABLE_VERIFICATION"
+    "FREERTOS_TCP_ENABLE_VERIFICATION",
+    "CBMC_GETNETWORKBUFFER_FAILURE_BOUND"
   ],
   "INC":
   [
diff --git a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c
index 00f6e8014..3d651a369 100644
--- a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c
+++ b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c
@@ -35,6 +35,81 @@ TaskHandle_t xTaskGetCurrentTaskHandle( void )
     return pxCurrentTCB;
 }
 
+/* Abstraction of vTCPStateChange */
+void vTCPStateChange( FreeRTOS_Socket_t * pxSocket,
+                      enum eTCP_STATE eTCPState )
+{
+}
+
+/* prvTCPReturnPacket is proven separately */
+void prvTCPReturnPacket( FreeRTOS_Socket_t * pxSocket,
+                         NetworkBufferDescriptor_t * pxDescriptor,
+                         uint32_t ulLen,
+                         BaseType_t xReleaseAfterSend )
+{
+    __CPROVER_assert( pxSocket != NULL, "pxSocket should not be NULL" );
+    __CPROVER_assert( pxDescriptor != NULL, "pxDescriptor should not be NULL" );
+    __CPROVER_assert( pxDescriptor->pucEthernetBuffer != NULL, "pucEthernetBuffer should not be NULL" );
+}
+
+/* prvTCPPrepareSend is proven separately. */
+int32_t prvTCPPrepareSend( FreeRTOS_Socket_t * pxSocket,
+                           NetworkBufferDescriptor_t ** ppxNetworkBuffer,
+                           UBaseType_t uxOptionsLength )
+{
+    __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" );
+    __CPROVER_assert( *ppxNetworkBuffer != NULL, "*ppxNetworkBuffer cannot be NULL" );
+    __CPROVER_assert( __CPROVER_r_ok( (*ppxNetworkBuffer)->pucEthernetBuffer, (*ppxNetworkBuffer)->xDataLength ), "Data in *ppxNetworkBuffer must be readable" );
+
+    return nondet_int32();
+}
+
+/* prvTCPHandleState is proven separately. */
+BaseType_t prvTCPHandleState( FreeRTOS_Socket_t * pxSocket,
+                              NetworkBufferDescriptor_t ** ppxNetworkBuffer )
+{
+    __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" );
+    __CPROVER_assert( *ppxNetworkBuffer != NULL, "*ppxNetworkBuffer cannot be NULL" );
+    __CPROVER_assert( __CPROVER_r_ok( (*ppxNetworkBuffer)->pucEthernetBuffer, (*ppxNetworkBuffer)->xDataLength ), "Data in *ppxNetworkBuffer must be readable" );
+
+    return nondet_basetype();
+}
+
+/* prvCheckOptions is proven separately. */
+BaseType_t prvCheckOptions( FreeRTOS_Socket_t * pxSocket,
+                            const NetworkBufferDescriptor_t * pxNetworkBuffer )
+{
+    __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" );
+    __CPROVER_assert( pxNetworkBuffer != NULL, "*ppxNetworkBuffer cannot be NULL" );
+    __CPROVER_assert( __CPROVER_r_ok( pxNetworkBuffer->pucEthernetBuffer, pxNetworkBuffer->xDataLength ), "Data in *ppxNetworkBuffer must be readable" );
+
+    return nondet_basetype();
+}
+
+BaseType_t xTCPWindowTxHasData( TCPWindow_t const * pxWindow,
+                                uint32_t ulWindowSize,
+                                TickType_t * pulDelay )
+{
+    __CPROVER_assert( pxWindow != NULL, "pxWindow cannot be NULL" );
+    __CPROVER_assert( pulDelay != NULL, "pulDelay cannot be NULL" );
+
+    return nondet_basetype();
+}
+
+/* Abstraction of xSequenceLessThan */
+BaseType_t xSequenceLessThan( uint32_t a,
+                              uint32_t b )
+{
+    return nondet_basetype();
+}
+
+/* Abstraction of xSequenceGreaterThan */
+BaseType_t xSequenceGreaterThan( uint32_t a,
+                                 uint32_t b )
+{
+    return nondet_basetype();
+}
+
 /* Abstraction of prvHandleListen_IPV4 */
 FreeRTOS_Socket_t * prvHandleListen_IPV4( FreeRTOS_Socket_t * pxSocket,
                                           NetworkBufferDescriptor_t * pxNetworkBuffer )
@@ -98,14 +173,12 @@ size_t uxIPHeaderSizeSocket( const FreeRTOS_Socket_t * pxSocket )
 
 void harness()
 {
-    NetworkBufferDescriptor_t * pxNetworkBuffer = safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
+    NetworkBufferDescriptor_t * pxNetworkBuffer;
+
+    pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( sizeof( TCPPacket_t ), 0 );
 
     /* To avoid asserting on the network buffer being NULL. */
     __CPROVER_assume( pxNetworkBuffer != NULL );
-
-    pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( TCPPacket_t ) );
-
-    /* To avoid asserting on the ethernet buffer being NULL. */
     __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
 
     xProcessReceivedTCPPacket( pxNetworkBuffer );
diff --git a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/Makefile.json b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/Makefile.json
index 53a28f733..c37bc279d 100644
--- a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/Makefile.json
+++ b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/Makefile.json
@@ -10,23 +10,17 @@
   [
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_IP.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_IP_IPv6.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_Transmission_IPv6.goto"
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_TCP_IP.goto"
   ],
   "INSTFLAGS":
   [
-    "--remove-function-body prvSingleStepTCPHeaderOptions",
-    "--remove-function-body prvCheckOptions",
-    "--remove-function-body prvTCPPrepareSend",
-    "--remove-function-body prvTCPReturnPacket",
-    "--remove-function-body prvTCPHandleState",
-    "--remove-function-body vTCPStateChange"
   ],
   "DEF":
   [
-    "FREERTOS_TCP_ENABLE_VERIFICATION"
+    "FREERTOS_TCP_ENABLE_VERIFICATION",
+    "CBMC_GETNETWORKBUFFER_FAILURE_BOUND"
   ],
   "INC":
   [
diff --git a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/ProcessReceivedTCPPacket_IPv6_harness.c b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/ProcessReceivedTCPPacket_IPv6_harness.c
index c2be060ce..4135a9144 100644
--- a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/ProcessReceivedTCPPacket_IPv6_harness.c
+++ b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket_IPv6/ProcessReceivedTCPPacket_IPv6_harness.c
@@ -99,20 +99,18 @@ size_t uxIPHeaderSizeSocket( const FreeRTOS_Socket_t * pxSocket )
 
 void harness()
 {
-    NetworkBufferDescriptor_t * pxNetworkBuffer = safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
+    NetworkBufferDescriptor_t * pxNetworkBuffer;
     EthernetHeader_t * pxEthernetHeader;
 
-    /* To avoid asserting on the network buffer being NULL. */
-    __CPROVER_assume( pxNetworkBuffer != NULL );
-
-    pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( TCPPacket_IPv6_t ) );
+    pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( sizeof( TCPPacket_IPv6_t ), 0 );
 
     /* To avoid asserting on the ethernet buffer being NULL. */
+    __CPROVER_assume( pxNetworkBuffer != NULL );
     __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
 
-    /* Ethernet frame type is checked before calling xProcessReceivedTCPPacket_IPV6. */
+    /* In this test case, we focus on IPv6 packets. */
     pxEthernetHeader = ( EthernetHeader_t * ) pxNetworkBuffer->pucEthernetBuffer;
     __CPROVER_assume( pxEthernetHeader->usFrameType == ipIPv6_FRAME_TYPE );
 
-    xProcessReceivedTCPPacket_IPV6( pxNetworkBuffer );
+    xProcessReceivedTCPPacket( pxNetworkBuffer );
 }
diff --git a/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json b/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json
index bc0bc61db..8c6859f4b 100644
--- a/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json
+++ b/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/Makefile.json
@@ -11,6 +11,8 @@
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
     "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_UDP_IP.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_UDP_IPv4.goto",
diff --git a/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c b/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c
index 6d282aca9..3c09124bb 100644
--- a/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c
+++ b/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c
@@ -9,6 +9,9 @@
 #include "FreeRTOS_UDP_IP.h"
 #include "FreeRTOS_TCP_IP.h"
 
+/* CBMC includes. */
+#include "cbmc.h"
+
 /*This proof assumes that pxUDPSocketLookup is implemented correctly. */
 
 /* This proof was done before. Hence we assume it to be correct here. */
@@ -17,6 +20,12 @@ void vARPRefreshCacheEntry( const MACAddress_t * pxMACAddress,
 {
 }
 
+void vARPRefreshCacheEntryAge( const MACAddress_t * pxMACAddress,
+                               const uint32_t ulIPAddress )
+{
+    __CPROVER_assert( pxMACAddress != NULL, "pxMACAddress cannot be NULL" );
+}
+
 /* This proof was done before. Hence we assume it to be correct here. */
 BaseType_t xIsDHCPSocket( Socket_t xSocket )
 {
@@ -68,19 +77,6 @@ BaseType_t xProcessReceivedUDPPacket_IPv6( NetworkBufferDescriptor_t * pxNetwork
     return xReturn;
 }
 
-/* Implementation of safe malloc */
-void * safeMalloc( size_t xWantedSize )
-{
-    if( xWantedSize == 0 )
-    {
-        return NULL;
-    }
-
-    uint8_t byte;
-
-    return byte ? malloc( xWantedSize ) : NULL;
-}
-
 /* Abstraction of pxUDPSocketLookup */
 FreeRTOS_Socket_t * pxUDPSocketLookup( UBaseType_t uxLocalPort )
 {
@@ -89,26 +85,23 @@ FreeRTOS_Socket_t * pxUDPSocketLookup( UBaseType_t uxLocalPort )
 
 void harness()
 {
-    NetworkBufferDescriptor_t * pxNetworkBuffer = safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
-    BaseType_t * pxIsWaitingForARPResolution;
+    NetworkBufferDescriptor_t * pxNetworkBuffer;
+    BaseType_t xIsWaitingForARPResolution;
     NetworkEndPoint_t xEndpoint;
     uint16_t usPort;
+    EthernetHeader_t * pxHeader;
 
-    pxIsWaitingForARPResolution = safeMalloc( sizeof( BaseType_t ) );
-
-    /* The function under test is only called by the IP-task. The below pointer is an
-     * address of a local variable which is being passed to the function under test.
-     * Thus, it cannot ever be NULL. */
-    __CPROVER_assume( pxIsWaitingForARPResolution != NULL );
-
+    pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( sizeof( UDPPacket_t ), 0 );
     /* The network buffer must not be NULL, checked in prvProcessEthernetPacket. */
     __CPROVER_assume( pxNetworkBuffer != NULL );
-
-    pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( UDPPacket_t ) );
+    __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
+    
     pxNetworkBuffer->pxEndPoint = &xEndpoint;
 
-    /* The ethernet buffer must be valid. */
-    __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
+    /* In this test case, we only focus on IPv4. */
+    pxHeader = ( ( const EthernetHeader_t * ) pxNetworkBuffer->pucEthernetBuffer );
+    __CPROVER_assume( pxHeader->usFrameType != ipIPv6_FRAME_TYPE );
 
-    xProcessReceivedUDPPacket( pxNetworkBuffer, usPort, pxIsWaitingForARPResolution );
+    xIsWaitingForARPResolution = nondet_BaseType();
+    xProcessReceivedUDPPacket( pxNetworkBuffer, usPort, &xIsWaitingForARPResolution );
 }

From 81c22a3aa158e1d8625940b5e1f051334c93d280 Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Tue, 16 Jul 2024 08:49:02 +0000
Subject: [PATCH 31/36] Fix DNSgetHostByName_cancel CBMC test

---
 .../DNSgetHostByName_cancel_harness.c         | 35 ++++++-------------
 .../DNS/DNSgetHostByName_cancel/Makefile.json | 17 +++++----
 2 files changed, 22 insertions(+), 30 deletions(-)

diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c
index 4ece6565b..a438cf629 100644
--- a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c
+++ b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c
@@ -8,11 +8,11 @@
 #include "FreeRTOS_DNS.h"
 #include "FreeRTOS_IP_Private.h"
 
+/* CBMC includes. */
+#include "cbmc.h"
 
 /* This proof assumes the length of pcHostName is bounded by MAX_HOSTNAME_LEN. This also abstracts the concurrency. */
-
 void vDNSInitialise( void );
-
 BaseType_t xDNSSetCallBack( const char * pcHostName,
                             void * pvSearchID,
                             FOnDNSEvent pCallbackFunction,
@@ -20,33 +20,18 @@ BaseType_t xDNSSetCallBack( const char * pcHostName,
                             TickType_t xIdentifier,
                             BaseType_t xIsIPv6 );
 
-void * safeMalloc( size_t xWantedSize ) /* Returns a NULL pointer if the wanted size is 0. */
-{
-    if( xWantedSize == 0 )
-    {
-        return NULL;
-    }
-
-    uint8_t byte;
-
-    return byte ? malloc( xWantedSize ) : NULL;
-}
-
-/* Abstraction of xTaskCheckForTimeOut from task pool. This also abstracts the concurrency. */
-BaseType_t xTaskCheckForTimeOut( TimeOut_t * const pxTimeOut,
-                                 TickType_t * const pxTicksToWait )
+/* The function func mimics the callback function.*/
+void func( const char * pcHostName,
+           void * pvSearchID,
+           uint32_t ulIPAddress )
 {
 }
 
-/* Abstraction of xTaskResumeAll from task pool. This also abstracts the concurrency. */
-BaseType_t xTaskResumeAll( void )
+void vDNSTimerReload( uint32_t ulCheckTime )
 {
 }
 
-/* The function func mimics the callback function.*/
-void func( const char * pcHostName,
-           void * pvSearchID,
-           uint32_t ulIPAddress )
+void vIPSetDNSTimerEnableState( BaseType_t xEnableState )
 {
 }
 
@@ -61,11 +46,13 @@ void harness()
     size_t len;
     BaseType_t xReturn;
 
-    __CPROVER_assume( len >= 0 && len <= MAX_HOSTNAME_LEN );
+    __CPROVER_assume( len > 0 && len <= MAX_HOSTNAME_LEN );
     char * pcHostName = safeMalloc( len );
+    __CPROVER_assume( pcHostName != NULL );
 
     if( len && pcHostName )
     {
+        __CPROVER_havoc_slice( pcHostName, len - 1 );
         pcHostName[ len - 1 ] = NULL;
     }
 
diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json
index 8f568fb54..7025729ed 100644
--- a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json
+++ b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json
@@ -4,20 +4,25 @@
 	# This configuration flag sets callback to 1. It also sets MAX_HOSTNAME_LEN to 10 for performance issues.
   # According to the specification MAX_HOST_NAME is upto 255.
   "callback": 1,
-  "MAX_HOSTNAME_LEN": 10,
+  "MAX_HOSTNAME_LEN": 3,
   "HOSTNAME_UNWIND": "__eval {MAX_HOSTNAME_LEN} + 1",
   "CBMCFLAGS":
   [
     "--unwind 1",
-    "--unwindset prvProcessDNSCache.0:5,strlen.0:{HOSTNAME_UNWIND},__builtin___strcpy_chk.0:{HOSTNAME_UNWIND},vDNSCheckCallBack.0:2,strcpy.0:{HOSTNAME_UNWIND}",
-    "--nondet-static"
+    "--unwindset strlen.0:{HOSTNAME_UNWIND}",
+    "--unwindset strncpy.0:{HOSTNAME_UNWIND}",
+    "--unwindset vDNSCheckCallBack.0:2"
   ],
   "OBJS":
   [
-    "$(ENTRY)_harness.goto",
+    "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto",
-    "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto",
-    "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto"
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Callback.goto",
+    "$(ENTRY)_harness.goto"
   ],
   "DEF":
   [

From e2bb4e5c4dce8db6a73789ceb8a2c9a4ce78fe93 Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Tue, 16 Jul 2024 08:55:53 +0000
Subject: [PATCH 32/36] Formatting

---
 source/FreeRTOS_IP.c                                      | 1 +
 .../DHCPv6HandleOption/DHCPv6HandleOption_harness.c       | 4 ++--
 .../ProcessICMPMessage_IPv6_harness.c                     | 2 +-
 .../ND/prvReturnICMP_IPv6/ReturnICMP_IPv6_harness.c       | 6 +++---
 .../proofs/Socket/lTCPAddRxdata/TCPAddRxdata_harness.c    | 1 +
 test/cbmc/proofs/TCP/prvSendData/SendData_harness.c       | 4 +++-
 .../proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c | 4 +++-
 .../proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c | 2 ++
 .../TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c      | 8 ++------
 .../TCPReturnPacket_IPv6_harness.c                        | 2 ++
 .../parsing/ProcessIPPacket/ProcessIPPacket_harness.c     | 6 +++---
 .../ProcessReceivedTCPPacket_harness.c                    | 4 ++--
 .../ProcessReceivedUDPPacket_harness.c                    | 2 +-
 test/cbmc/stubs/freertos_api.c                            | 1 -
 test/cbmc/stubs/freertos_kernel_api.c                     | 1 +
 15 files changed, 27 insertions(+), 21 deletions(-)

diff --git a/source/FreeRTOS_IP.c b/source/FreeRTOS_IP.c
index 54b3e0d39..96e894e52 100644
--- a/source/FreeRTOS_IP.c
+++ b/source/FreeRTOS_IP.c
@@ -1042,6 +1042,7 @@ void FreeRTOS_ReleaseUDPPayloadBuffer( void const * pvBuffer )
     NetworkBufferDescriptor_t * pxBuffer;
 
     pxBuffer = pxUDPPayloadBuffer_to_NetworkBuffer( pvBuffer );
+
     if( pxBuffer != NULL )
     {
         vReleaseNetworkBufferAndDescriptor( pxBuffer );
diff --git a/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/DHCPv6HandleOption_harness.c b/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/DHCPv6HandleOption_harness.c
index 5800b6082..96b30b73c 100644
--- a/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/DHCPv6HandleOption_harness.c
+++ b/test/cbmc/proofs/DHCPv6/DHCPv6HandleOption/DHCPv6HandleOption_harness.c
@@ -76,12 +76,12 @@ BaseType_t __CPROVER_file_local_FreeRTOS_DHCPv6_c_prvDHCPv6_subOption( uint16_t
 
 uint16_t usBitConfig_read_16( BitConfig_t * pxConfig )
 {
-    return (uint16_t) nondet_uint32();
+    return ( uint16_t ) nondet_uint32();
 }
 
 uint8_t ucBitConfig_read_8( BitConfig_t * pxConfig )
 {
-    return (uint8_t) nondet_uint32();
+    return ( uint8_t ) nondet_uint32();
 }
 
 BaseType_t xBitConfig_read_uc( BitConfig_t * pxConfig,
diff --git a/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/ProcessICMPMessage_IPv6_harness.c b/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/ProcessICMPMessage_IPv6_harness.c
index 3efb55b4c..0b02ac8ed 100644
--- a/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/ProcessICMPMessage_IPv6_harness.c
+++ b/test/cbmc/proofs/ND/prvProcessICMPMessage_IPv6/ProcessICMPMessage_IPv6_harness.c
@@ -124,7 +124,7 @@ NetworkEndPoint_t * FreeRTOS_InterfaceEPInSameSubnet_IPv6( const NetworkInterfac
 size_t uxIPHeaderSizePacket( const NetworkBufferDescriptor_t * pxNetworkBuffer )
 {
     size_t uxResult;
-    
+
     __CPROVER_assume( ( uxResult == ipSIZE_OF_IPv4_HEADER ) || ( uxResult == ipSIZE_OF_IPv6_HEADER ) );
 
     return uxResult;
diff --git a/test/cbmc/proofs/ND/prvReturnICMP_IPv6/ReturnICMP_IPv6_harness.c b/test/cbmc/proofs/ND/prvReturnICMP_IPv6/ReturnICMP_IPv6_harness.c
index 1c072f6f1..e0340a76c 100644
--- a/test/cbmc/proofs/ND/prvReturnICMP_IPv6/ReturnICMP_IPv6_harness.c
+++ b/test/cbmc/proofs/ND/prvReturnICMP_IPv6/ReturnICMP_IPv6_harness.c
@@ -127,7 +127,7 @@ NetworkEndPoint_t * FreeRTOS_InterfaceEPInSameSubnet_IPv6( const NetworkInterfac
 size_t uxIPHeaderSizePacket( const NetworkBufferDescriptor_t * pxNetworkBuffer )
 {
     size_t uxResult;
-    
+
     __CPROVER_assume( ( uxResult == ipSIZE_OF_IPv4_HEADER ) || ( uxResult == ipSIZE_OF_IPv6_HEADER ) );
 
     return uxResult;
@@ -137,11 +137,11 @@ void harness()
 {
     NetworkBufferDescriptor_t * pxNetworkBuffer;
     uint32_t ulLen;
-    NetworkBufferDescriptor_t *pxLocalARPWaitingNetworkBuffer;
+    NetworkBufferDescriptor_t * pxLocalARPWaitingNetworkBuffer;
     uint16_t usEthernetBufferSize;
 
     __CPROVER_assume( ( ulLen >= sizeof( ICMPPacket_IPv6_t ) ) && ( ulLen < ipconfigNETWORK_MTU ) );
-    
+
     pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( ulLen, 0 );
 
     /* The code does not expect pxNetworkBuffer to be NULL. */
diff --git a/test/cbmc/proofs/Socket/lTCPAddRxdata/TCPAddRxdata_harness.c b/test/cbmc/proofs/Socket/lTCPAddRxdata/TCPAddRxdata_harness.c
index 4fefc1d10..123b94527 100644
--- a/test/cbmc/proofs/Socket/lTCPAddRxdata/TCPAddRxdata_harness.c
+++ b/test/cbmc/proofs/Socket/lTCPAddRxdata/TCPAddRxdata_harness.c
@@ -37,6 +37,7 @@ void * pvPortMallocLarge( size_t xWantedSize )
 size_t uxStreamBufferFrontSpace( const StreamBuffer_t * const pxBuffer )
 {
     size_t uxReturn;
+
     return uxReturn;
 }
 
diff --git a/test/cbmc/proofs/TCP/prvSendData/SendData_harness.c b/test/cbmc/proofs/TCP/prvSendData/SendData_harness.c
index bfd3bde04..1f76a23fc 100644
--- a/test/cbmc/proofs/TCP/prvSendData/SendData_harness.c
+++ b/test/cbmc/proofs/TCP/prvSendData/SendData_harness.c
@@ -84,6 +84,7 @@ FreeRTOS_Socket_t * ensure_FreeRTOS_Socket_t_is_allocated()
     pxSocket->u.xTCP.pxPeerSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) );
     pxSocket->pxEndPoint = safeMalloc( sizeof( NetworkEndPoint_t ) );
     pxSocket->u.xTCP.pxAckMessage = safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
+
     if( pxSocket->u.xTCP.pxAckMessage != NULL )
     {
         __CPROVER_assume( ( buf_size > ( ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + sizeof( TCPHeader_t ) ) ) && ( buf_size < ipconfigNETWORK_MTU ) );
@@ -94,7 +95,7 @@ FreeRTOS_Socket_t * ensure_FreeRTOS_Socket_t_is_allocated()
     return pxSocket;
 }
 
-/* 
+/*
  * In this function, it only allocates network buffer by harness.
  */
 void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer )
@@ -106,6 +107,7 @@ void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNet
     {
         free( pxNetworkBuffer->pucEthernetBuffer );
     }
+
     free( pxNetworkBuffer );
 }
 
diff --git a/test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c b/test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c
index 8107322b3..c73802300 100644
--- a/test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c
+++ b/test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c
@@ -88,6 +88,7 @@ FreeRTOS_Socket_t * ensure_FreeRTOS_Socket_t_is_allocated()
     pxSocket->u.xTCP.pxPeerSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) );
     pxSocket->pxEndPoint = safeMalloc( sizeof( NetworkEndPoint_t ) );
     pxSocket->u.xTCP.pxAckMessage = safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
+
     if( pxSocket->u.xTCP.pxAckMessage != NULL )
     {
         __CPROVER_assume( ( buf_size > ( ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + sizeof( TCPHeader_t ) ) ) && ( buf_size < ipconfigNETWORK_MTU ) );
@@ -140,7 +141,7 @@ int32_t lTCPWindowRxCheck( TCPWindow_t * pxWindow,
     __CPROVER_assert( pxWindow != NULL, "pxWindow cannot be NULL" );
     __CPROVER_assert( __CPROVER_r_ok( pxWindow, sizeof( TCPWindow_t ) ), "pxWindow must be readable" );
     *pulSkipCount = nondet_uint32();
-    
+
     return nondet_int32();
 }
 
@@ -245,6 +246,7 @@ void harness()
     FreeRTOS_Socket_t * pxSocket = ensure_FreeRTOS_Socket_t_is_allocated();
 
     __CPROVER_assume( pxSocket != NULL );
+
     /* ucOptionLength is the number of valid bytes in ulOptionsData[].
      * ulOptionsData[] is initialized as uint32_t ulOptionsData[ipSIZE_TCP_OPTIONS/sizeof(uint32_t)].
      * This assumption is required for a memcpy function that copies uxOptionsLength
diff --git a/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c b/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c
index 6a84f09e0..63bfac279 100644
--- a/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c
+++ b/test/cbmc/proofs/TCP/prvTCPPrepareSend/TCPPrepareSend_harness.c
@@ -56,6 +56,7 @@ FreeRTOS_Socket_t * ensure_FreeRTOS_Socket_t_is_allocated()
     pxSocket->u.xTCP.pxPeerSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) );
     pxSocket->pxEndPoint = safeMalloc( sizeof( NetworkEndPoint_t ) );
     pxSocket->u.xTCP.pxAckMessage = safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
+
     if( pxSocket->u.xTCP.pxAckMessage != NULL )
     {
         __CPROVER_assume( ( buf_size > ( ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + sizeof( TCPHeader_t ) ) ) && ( buf_size < ipconfigNETWORK_MTU ) );
@@ -90,6 +91,7 @@ uint32_t ulTCPWindowTxGet( TCPWindow_t * pxWindow,
                            int32_t * plPosition )
 {
     uint32_t ulReturn = nondet_uint32();
+
     __CPROVER_assert( pxWindow != NULL, "pxWindow cannot be NULL" );
     __CPROVER_assert( plPosition != NULL, "plPosition cannot be NULL" );
 
diff --git a/test/cbmc/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c b/test/cbmc/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c
index 6bed552f2..da15dfe89 100644
--- a/test/cbmc/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c
+++ b/test/cbmc/proofs/TCP/prvTCPReturnPacket/TCPReturnPacket_harness.c
@@ -62,6 +62,7 @@ FreeRTOS_Socket_t * ensure_FreeRTOS_Socket_t_is_allocated()
     pxSocket->u.xTCP.pxPeerSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) );
     pxSocket->pxEndPoint = safeMalloc( sizeof( NetworkEndPoint_t ) );
     pxSocket->u.xTCP.pxAckMessage = safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
+
     if( pxSocket->u.xTCP.pxAckMessage != NULL )
     {
         __CPROVER_assume( ( buf_size > ( ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + sizeof( TCPHeader_t ) ) ) && ( buf_size < ipconfigNETWORK_MTU ) );
@@ -211,18 +212,13 @@ void harness()
     EthernetHeader_t * pxHeader;
 
     pxSocket = ensure_FreeRTOS_Socket_t_is_allocated();
+
     if( pxSocket != NULL )
     {
         /* In this test case, we only focus on IPv4. */
         __CPROVER_assume( pxSocket->bits.bIsIPv6 == pdFALSE_UNSIGNED );
     }
 
-    // if( pxSocket->u.xTCP.bits.bReuseSocket == pdFALSE )
-    // {
-    //     /* Make sure we have parent socket if reuse is set to FALSE to avoid assertion in vTCPStateChange(). */
-    //     __CPROVER_assume( pxSocket->u.xTCP.pxPeerSocket != NULL );
-    // }
-
     __CPROVER_assume( ( ulLen >= sizeof( TCPPacket_t ) ) && ( ulLen < ipconfigNETWORK_MTU - ipSIZE_OF_ETH_HEADER ) );
     pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( ulLen + ipSIZE_OF_ETH_HEADER, 0 );
 
diff --git a/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/TCPReturnPacket_IPv6_harness.c b/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/TCPReturnPacket_IPv6_harness.c
index b029febce..95f47538c 100644
--- a/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/TCPReturnPacket_IPv6_harness.c
+++ b/test/cbmc/proofs/TCP/prvTCPReturnPacket_IPv6/TCPReturnPacket_IPv6_harness.c
@@ -75,6 +75,7 @@ FreeRTOS_Socket_t * ensure_FreeRTOS_Socket_t_is_allocated()
     pxSocket->u.xTCP.pxPeerSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) );
     pxSocket->pxEndPoint = safeMalloc( sizeof( NetworkEndPoint_t ) );
     pxSocket->u.xTCP.pxAckMessage = safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
+
     if( pxSocket->u.xTCP.pxAckMessage != NULL )
     {
         __CPROVER_assume( ( buf_size > ( ipSIZE_OF_ETH_HEADER + ipSIZE_OF_IPv6_HEADER + sizeof( TCPHeader_t ) ) ) && ( buf_size < ipconfigNETWORK_MTU ) );
@@ -190,6 +191,7 @@ void harness()
     EthernetHeader_t * pxHeader;
 
     pxSocket = ensure_FreeRTOS_Socket_t_is_allocated();
+
     if( pxSocket != NULL )
     {
         /* In this test case, we only focus on IPv6. */
diff --git a/test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c b/test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c
index bfa47ad81..e8c498ac9 100644
--- a/test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c
+++ b/test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c
@@ -45,7 +45,7 @@ BaseType_t xGetExtensionOrder( uint8_t ucProtocol,
 BaseType_t xCheckRequiresARPResolution( const NetworkBufferDescriptor_t * pxNetworkBuffer )
 {
     BaseType_t xReturn;
-    
+
     __CPROVER_assert( pxNetworkBuffer != NULL, "pxNetworkBuffer cannot be NULL" );
     __CPROVER_assert( __CPROVER_r_ok( pxNetworkBuffer->pucEthernetBuffer, pxNetworkBuffer->xDataLength ), "Data in pxNetworkBuffer must be readable" );
 }
@@ -82,7 +82,7 @@ NetworkEndPoint_t * FreeRTOS_FindEndPointOnIP_IPv4( uint32_t ulIPAddress,
 eFrameProcessingResult_t ProcessICMPPacket( const NetworkBufferDescriptor_t * const pxNetworkBuffer )
 {
     eFrameProcessingResult_t xReturn;
-    
+
     __CPROVER_assert( pxNetworkBuffer != NULL, "pxEndPoint cannot be NULL" );
     __CPROVER_assert( __CPROVER_r_ok( pxNetworkBuffer->pucEthernetBuffer, pxNetworkBuffer->xDataLength ), "Data in pxNetworkBuffer must be readable" );
 
@@ -93,7 +93,7 @@ eFrameProcessingResult_t ProcessICMPPacket( const NetworkBufferDescriptor_t * co
 eFrameProcessingResult_t prvProcessICMPMessage_IPv6( NetworkBufferDescriptor_t * const pxNetworkBuffer )
 {
     eFrameProcessingResult_t xReturn;
-    
+
     __CPROVER_assert( pxNetworkBuffer != NULL, "pxEndPoint cannot be NULL" );
     __CPROVER_assert( __CPROVER_r_ok( pxNetworkBuffer->pucEthernetBuffer, pxNetworkBuffer->xDataLength ), "Data in pxNetworkBuffer must be readable" );
 
diff --git a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c
index 3d651a369..c15387b90 100644
--- a/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c
+++ b/test/cbmc/proofs/parsing/ProcessReceivedTCPPacket/ProcessReceivedTCPPacket_harness.c
@@ -59,7 +59,7 @@ int32_t prvTCPPrepareSend( FreeRTOS_Socket_t * pxSocket,
 {
     __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" );
     __CPROVER_assert( *ppxNetworkBuffer != NULL, "*ppxNetworkBuffer cannot be NULL" );
-    __CPROVER_assert( __CPROVER_r_ok( (*ppxNetworkBuffer)->pucEthernetBuffer, (*ppxNetworkBuffer)->xDataLength ), "Data in *ppxNetworkBuffer must be readable" );
+    __CPROVER_assert( __CPROVER_r_ok( ( *ppxNetworkBuffer )->pucEthernetBuffer, ( *ppxNetworkBuffer )->xDataLength ), "Data in *ppxNetworkBuffer must be readable" );
 
     return nondet_int32();
 }
@@ -70,7 +70,7 @@ BaseType_t prvTCPHandleState( FreeRTOS_Socket_t * pxSocket,
 {
     __CPROVER_assert( pxSocket != NULL, "pxSocket cannot be NULL" );
     __CPROVER_assert( *ppxNetworkBuffer != NULL, "*ppxNetworkBuffer cannot be NULL" );
-    __CPROVER_assert( __CPROVER_r_ok( (*ppxNetworkBuffer)->pucEthernetBuffer, (*ppxNetworkBuffer)->xDataLength ), "Data in *ppxNetworkBuffer must be readable" );
+    __CPROVER_assert( __CPROVER_r_ok( ( *ppxNetworkBuffer )->pucEthernetBuffer, ( *ppxNetworkBuffer )->xDataLength ), "Data in *ppxNetworkBuffer must be readable" );
 
     return nondet_basetype();
 }
diff --git a/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c b/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c
index 3c09124bb..0b2b8c14c 100644
--- a/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c
+++ b/test/cbmc/proofs/parsing/ProcessReceivedUDPPacket/ProcessReceivedUDPPacket_harness.c
@@ -95,7 +95,7 @@ void harness()
     /* The network buffer must not be NULL, checked in prvProcessEthernetPacket. */
     __CPROVER_assume( pxNetworkBuffer != NULL );
     __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
-    
+
     pxNetworkBuffer->pxEndPoint = &xEndpoint;
 
     /* In this test case, we only focus on IPv4. */
diff --git a/test/cbmc/stubs/freertos_api.c b/test/cbmc/stubs/freertos_api.c
index 8d068614c..db349a25a 100644
--- a/test/cbmc/stubs/freertos_api.c
+++ b/test/cbmc/stubs/freertos_api.c
@@ -409,7 +409,6 @@ BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxNetworkB
 ****************************************************************/
 void vIPSetARPResolutionTimerEnableState( BaseType_t xEnableState )
 {
-
 }
 
 /****************************************************************/
diff --git a/test/cbmc/stubs/freertos_kernel_api.c b/test/cbmc/stubs/freertos_kernel_api.c
index fab4c7c98..79fd0ff82 100644
--- a/test/cbmc/stubs/freertos_kernel_api.c
+++ b/test/cbmc/stubs/freertos_kernel_api.c
@@ -96,6 +96,7 @@ void vEventGroupDelete( EventGroupHandle_t xEventGroup )
 EventGroupHandle_t xEventGroupCreate( void )
 {
     EventGroupHandle_t xReturn;
+
     return xReturn;
 }
 

From 274ea9e357f559295e27307729270245a93f9b84 Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Tue, 16 Jul 2024 09:39:09 +0000
Subject: [PATCH 33/36] Revert "Fix DNSgetHostByName_cancel CBMC test"

This reverts commit 81c22a3aa158e1d8625940b5e1f051334c93d280.
---
 .../DNSgetHostByName_cancel_harness.c         | 35 +++++++++++++------
 .../DNS/DNSgetHostByName_cancel/Makefile.json | 17 ++++-----
 2 files changed, 30 insertions(+), 22 deletions(-)

diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c
index a438cf629..4ece6565b 100644
--- a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c
+++ b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c
@@ -8,11 +8,11 @@
 #include "FreeRTOS_DNS.h"
 #include "FreeRTOS_IP_Private.h"
 
-/* CBMC includes. */
-#include "cbmc.h"
 
 /* This proof assumes the length of pcHostName is bounded by MAX_HOSTNAME_LEN. This also abstracts the concurrency. */
+
 void vDNSInitialise( void );
+
 BaseType_t xDNSSetCallBack( const char * pcHostName,
                             void * pvSearchID,
                             FOnDNSEvent pCallbackFunction,
@@ -20,18 +20,33 @@ BaseType_t xDNSSetCallBack( const char * pcHostName,
                             TickType_t xIdentifier,
                             BaseType_t xIsIPv6 );
 
-/* The function func mimics the callback function.*/
-void func( const char * pcHostName,
-           void * pvSearchID,
-           uint32_t ulIPAddress )
+void * safeMalloc( size_t xWantedSize ) /* Returns a NULL pointer if the wanted size is 0. */
+{
+    if( xWantedSize == 0 )
+    {
+        return NULL;
+    }
+
+    uint8_t byte;
+
+    return byte ? malloc( xWantedSize ) : NULL;
+}
+
+/* Abstraction of xTaskCheckForTimeOut from task pool. This also abstracts the concurrency. */
+BaseType_t xTaskCheckForTimeOut( TimeOut_t * const pxTimeOut,
+                                 TickType_t * const pxTicksToWait )
 {
 }
 
-void vDNSTimerReload( uint32_t ulCheckTime )
+/* Abstraction of xTaskResumeAll from task pool. This also abstracts the concurrency. */
+BaseType_t xTaskResumeAll( void )
 {
 }
 
-void vIPSetDNSTimerEnableState( BaseType_t xEnableState )
+/* The function func mimics the callback function.*/
+void func( const char * pcHostName,
+           void * pvSearchID,
+           uint32_t ulIPAddress )
 {
 }
 
@@ -46,13 +61,11 @@ void harness()
     size_t len;
     BaseType_t xReturn;
 
-    __CPROVER_assume( len > 0 && len <= MAX_HOSTNAME_LEN );
+    __CPROVER_assume( len >= 0 && len <= MAX_HOSTNAME_LEN );
     char * pcHostName = safeMalloc( len );
-    __CPROVER_assume( pcHostName != NULL );
 
     if( len && pcHostName )
     {
-        __CPROVER_havoc_slice( pcHostName, len - 1 );
         pcHostName[ len - 1 ] = NULL;
     }
 
diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json
index 7025729ed..8f568fb54 100644
--- a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json
+++ b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json
@@ -4,25 +4,20 @@
 	# This configuration flag sets callback to 1. It also sets MAX_HOSTNAME_LEN to 10 for performance issues.
   # According to the specification MAX_HOST_NAME is upto 255.
   "callback": 1,
-  "MAX_HOSTNAME_LEN": 3,
+  "MAX_HOSTNAME_LEN": 10,
   "HOSTNAME_UNWIND": "__eval {MAX_HOSTNAME_LEN} + 1",
   "CBMCFLAGS":
   [
     "--unwind 1",
-    "--unwindset strlen.0:{HOSTNAME_UNWIND}",
-    "--unwindset strncpy.0:{HOSTNAME_UNWIND}",
-    "--unwindset vDNSCheckCallBack.0:2"
+    "--unwindset prvProcessDNSCache.0:5,strlen.0:{HOSTNAME_UNWIND},__builtin___strcpy_chk.0:{HOSTNAME_UNWIND},vDNSCheckCallBack.0:2,strcpy.0:{HOSTNAME_UNWIND}",
+    "--nondet-static"
   ],
   "OBJS":
   [
-    "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto",
-    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto",
-    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto",
+    "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Callback.goto",
-    "$(ENTRY)_harness.goto"
+    "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto",
+    "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto"
   ],
   "DEF":
   [

From e561de7a4b8eac7a80388fa8532a0ac5b1afec34 Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Tue, 16 Jul 2024 10:25:05 +0000
Subject: [PATCH 34/36] Fix DNSgetHostByName_cancel CBMC test

---
 .../DNSgetHostByName_cancel_harness.c         | 50 +++++++++++--------
 .../DNS/DNSgetHostByName_cancel/Makefile.json | 10 ++--
 2 files changed, 37 insertions(+), 23 deletions(-)

diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c
index 4ece6565b..217fe1b6f 100644
--- a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c
+++ b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c
@@ -8,6 +8,8 @@
 #include "FreeRTOS_DNS.h"
 #include "FreeRTOS_IP_Private.h"
 
+/* CBMC includes. */
+#include "cbmc.h"
 
 /* This proof assumes the length of pcHostName is bounded by MAX_HOSTNAME_LEN. This also abstracts the concurrency. */
 
@@ -20,27 +22,37 @@ BaseType_t xDNSSetCallBack( const char * pcHostName,
                             TickType_t xIdentifier,
                             BaseType_t xIsIPv6 );
 
-void * safeMalloc( size_t xWantedSize ) /* Returns a NULL pointer if the wanted size is 0. */
+/* Abstraction of uxListRemove from list. This also abstracts the concurrency. */
+void vListInitialise( List_t * const pxList )
 {
-    if( xWantedSize == 0 )
-    {
-        return NULL;
-    }
+    __CPROVER_assert( pxList != NULL, "pxList cannot be NULL" );
 
-    uint8_t byte;
+    pxList->pxIndex = ( ListItem_t * ) &( pxList->xListEnd );
+    pxList->xListEnd.xItemValue = portMAX_DELAY;
 
-    return byte ? malloc( xWantedSize ) : NULL;
+    /* The list end next and previous pointers point to itself so we know
+     * when the list is empty. */
+    pxList->xListEnd.pxNext = ( ListItem_t * ) &( pxList->xListEnd );
+    pxList->xListEnd.pxPrevious = ( ListItem_t * ) &( pxList->xListEnd );
+    pxList->uxNumberOfItems = ( UBaseType_t ) 0U;
 }
 
-/* Abstraction of xTaskCheckForTimeOut from task pool. This also abstracts the concurrency. */
-BaseType_t xTaskCheckForTimeOut( TimeOut_t * const pxTimeOut,
-                                 TickType_t * const pxTicksToWait )
+/* Abstraction of uxListRemove from list. This also abstracts the concurrency. */
+UBaseType_t uxListRemove( ListItem_t * const pxItemToRemove )
 {
-}
+    List_t * const pxList = pxItemToRemove->pxContainer;
+    pxItemToRemove->pxNext->pxPrevious = pxItemToRemove->pxPrevious;
+    pxItemToRemove->pxPrevious->pxNext = pxItemToRemove->pxNext;
 
-/* Abstraction of xTaskResumeAll from task pool. This also abstracts the concurrency. */
-BaseType_t xTaskResumeAll( void )
-{
+    if( pxList->pxIndex == pxItemToRemove )
+    {
+        pxList->pxIndex = pxItemToRemove->pxPrevious;
+    }
+
+    pxItemToRemove->pxContainer = NULL;
+    ( pxList->uxNumberOfItems )--;
+
+    return pxList->uxNumberOfItems;
 }
 
 /* The function func mimics the callback function.*/
@@ -61,13 +73,11 @@ void harness()
     size_t len;
     BaseType_t xReturn;
 
-    __CPROVER_assume( len >= 0 && len <= MAX_HOSTNAME_LEN );
+    __CPROVER_assume( len > 0 && len <= MAX_HOSTNAME_LEN );
     char * pcHostName = safeMalloc( len );
-
-    if( len && pcHostName )
-    {
-        pcHostName[ len - 1 ] = NULL;
-    }
+    __CPROVER_assume( pcHostName != NULL );
+    __CPROVER_havoc_slice( pcHostName, len - 1 );
+    pcHostName[ len - 1 ] = NULL;
 
     xReturn = xDNSSetCallBack( pcHostName, &pvSearchID, pCallback, xTimeout, xIdentifier, xIsIPv6 ); /* Add an item to be able to check the cancel function if the list is non-empty. */
     FreeRTOS_gethostbyname_cancel( &pvSearchID );
diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json
index 8f568fb54..fc7bfc4c0 100644
--- a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json
+++ b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/Makefile.json
@@ -10,14 +10,18 @@
   [
     "--unwind 1",
     "--unwindset prvProcessDNSCache.0:5,strlen.0:{HOSTNAME_UNWIND},__builtin___strcpy_chk.0:{HOSTNAME_UNWIND},vDNSCheckCallBack.0:2,strcpy.0:{HOSTNAME_UNWIND}",
-    "--nondet-static"
+    "--unwindset strncpy.0:{HOSTNAME_UNWIND}"
   ],
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Timers.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto",
-    "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/tasks.goto",
-    "$(FREERTOS_PLUS_TCP)/test/FreeRTOS-Kernel/list.goto"
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Callback.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_kernel_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto",
+    "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto"
   ],
   "DEF":
   [

From 607147670ac66f3a8ba735e26b64015fa95af15b Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Tue, 16 Jul 2024 10:28:42 +0000
Subject: [PATCH 35/36] Formatting

---
 .../DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c    | 1 +
 1 file changed, 1 insertion(+)

diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c
index 217fe1b6f..e4ec2ecff 100644
--- a/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c
+++ b/test/cbmc/proofs/DNS/DNSgetHostByName_cancel/DNSgetHostByName_cancel_harness.c
@@ -41,6 +41,7 @@ void vListInitialise( List_t * const pxList )
 UBaseType_t uxListRemove( ListItem_t * const pxItemToRemove )
 {
     List_t * const pxList = pxItemToRemove->pxContainer;
+
     pxItemToRemove->pxNext->pxPrevious = pxItemToRemove->pxPrevious;
     pxItemToRemove->pxPrevious->pxNext = pxItemToRemove->pxNext;
 

From f211db93d928c21532594ef8cd349ab1b0ee2eba Mon Sep 17 00:00:00 2001
From: ActoryOu <ousc@amazon.com>
Date: Tue, 16 Jul 2024 12:00:39 +0000
Subject: [PATCH 36/36] Revert unnecessary change

---
 source/FreeRTOS_IP.c                          |   7 +-
 source/FreeRTOS_IP_Utils.c                    |  34 ++---
 .../DNSgetHostByName_harness.c                | 129 ++++++++++--------
 .../proofs/DNS/DNSgetHostByName/Makefile.json |   2 +-
 .../DNSgetHostByName_a_harness.c              | 114 ++++++++--------
 .../DNS/DNSgetHostByName_a/Makefile.json      |   1 -
 6 files changed, 153 insertions(+), 134 deletions(-)

diff --git a/source/FreeRTOS_IP.c b/source/FreeRTOS_IP.c
index 96e894e52..3765e85a4 100644
--- a/source/FreeRTOS_IP.c
+++ b/source/FreeRTOS_IP.c
@@ -1042,11 +1042,8 @@ void FreeRTOS_ReleaseUDPPayloadBuffer( void const * pvBuffer )
     NetworkBufferDescriptor_t * pxBuffer;
 
     pxBuffer = pxUDPPayloadBuffer_to_NetworkBuffer( pvBuffer );
-
-    if( pxBuffer != NULL )
-    {
-        vReleaseNetworkBufferAndDescriptor( pxBuffer );
-    }
+    configASSERT( pxBuffer != NULL );
+    vReleaseNetworkBufferAndDescriptor( pxBuffer );
 }
 /*-----------------------------------------------------------*/
 
diff --git a/source/FreeRTOS_IP_Utils.c b/source/FreeRTOS_IP_Utils.c
index c9e64b857..3c27eb8bc 100644
--- a/source/FreeRTOS_IP_Utils.c
+++ b/source/FreeRTOS_IP_Utils.c
@@ -747,32 +747,32 @@ NetworkBufferDescriptor_t * pxUDPPayloadBuffer_to_NetworkBuffer( const void * pv
          * for a IPv6 packet, pucIPType will point to the first byte of the IP-header: 'ucVersionTrafficClass'. */
         ucIPType = pucIPType[ 0 ] & 0xf0U;
 
+        /* To help the translation from a UDP payload pointer to a networkBuffer,
+         * a byte was stored at a certain negative offset (-48 bytes).
+         * It must have a value of either 0x4x or 0x6x. */
+        configASSERT( ( ucIPType == ipTYPE_IPv4 ) || ( ucIPType == ipTYPE_IPv6 ) );
+
         switch( ucIPType ) /* LCOV_EXCL_BR_LINE */
         {
-            /* For Rx path, it's possible to receive packets that is disabled. We should be able to get the network
-             * descriptor to free that network buffer correctly. */
-            case ipTYPE_IPv6:
-                uxOffset = sizeof( UDPPacket_IPv6_t );
-                break;
+            #if ( ipconfigUSE_IPv6 != 0 )
+                case ipTYPE_IPv6:
+                    uxOffset = sizeof( UDPPacket_IPv6_t );
+                    break;
+            #endif /* ( ipconfigUSE_IPv6 != 0 ) */
 
-            case ipTYPE_IPv4:
-                uxOffset = sizeof( UDPPacket_t );
-                break;
+            #if ( ipconfigUSE_IPv4 != 0 )
+                case ipTYPE_IPv4:
+                    uxOffset = sizeof( UDPPacket_t );
+                    break;
+            #endif /* ( ipconfigUSE_IPv4 != 0 ) */
 
             default:
                 FreeRTOS_debug_printf( ( "pxUDPPayloadBuffer_to_NetworkBuffer: Undefined ucIPType \n" ) );
-                uxOffset = 0;
+                uxOffset = sizeof( UDPPacket_t );
                 break;
         }
 
-        if( uxOffset != 0 )
-        {
-            pxResult = prvPacketBuffer_to_NetworkBuffer( pvBuffer, uxOffset );
-        }
-        else
-        {
-            pxResult = NULL;
-        }
+        pxResult = prvPacketBuffer_to_NetworkBuffer( pvBuffer, uxOffset );
     }
 
     return pxResult;
diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c
index 71b53cee8..9e5658074 100644
--- a/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c
+++ b/test/cbmc/proofs/DNS/DNSgetHostByName/DNSgetHostByName_harness.c
@@ -17,6 +17,7 @@
 #include "NetworkBufferManagement.h"
 #include "NetworkInterface.h"
 
+/* CBMC includes. */
 #include "cbmc.h"
 
 uint32_t FreeRTOS_dnslookup( const char * pcHostName );
@@ -37,6 +38,7 @@ size_t __CPROVER_file_local_FreeRTOS_DNS_c_prvCreateDNSMessage( uint8_t * pucUDP
                                                                 const char * pcHostName,
                                                                 TickType_t uxIdentifier,
                                                                 UBaseType_t uxHostType );
+uintptr_t __CPROVER_file_local_FreeRTOS_IP_Utils_c_void_ptr_to_uintptr( const void * pvPointer );
 
 /****************************************************************
 * We abstract:
@@ -56,6 +58,54 @@ size_t __CPROVER_file_local_FreeRTOS_DNS_c_prvCreateDNSMessage( uint8_t * pucUDP
 * bound the iterations of strcmp.
 ****************************************************************/
 
+/*We assume that the pxGetNetworkBufferWithDescriptor function is implemented correctly and returns a valid data structure. */
+/*This is the mock to mimic the correct expected behavior. If this allocation fails, this might invalidate the proof. */
+NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes,
+                                                              TickType_t xBlockTimeTicks )
+{
+    NetworkBufferDescriptor_t * pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
+
+    if( pxNetworkBuffer != NULL )
+    {
+        pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xRequestedSizeBytes + ipUDP_PAYLOAD_IP_TYPE_OFFSET );
+
+        if( pxNetworkBuffer->pucEthernetBuffer == NULL )
+        {
+            free( pxNetworkBuffer );
+            pxNetworkBuffer = NULL;
+        }
+        else
+        {
+            pxNetworkBuffer->pucEthernetBuffer = ( ( uint8_t * ) pxNetworkBuffer->pucEthernetBuffer ) + ipUDP_PAYLOAD_IP_TYPE_OFFSET;
+            pxNetworkBuffer->xDataLength = xRequestedSizeBytes;
+        }
+    }
+
+    return pxNetworkBuffer;
+}
+
+/*
+ * In this function, it only allocates network buffer by pxGetNetworkBufferWithDescriptor
+ * stub function above here. In this case, we should free both network buffer descriptor and pucEthernetBuffer.
+ */
+void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer )
+{
+    __CPROVER_assert( pxNetworkBuffer != NULL,
+                      "Precondition: pxNetworkBuffer != NULL" );
+
+    free( pxNetworkBuffer->pucEthernetBuffer - ipUDP_PAYLOAD_IP_TYPE_OFFSET );
+    free( pxNetworkBuffer );
+}
+
+/* FreeRTOS_ReleaseUDPPayloadBuffer is mocked here and the memory
+ * is not freed as the buffer allocated by the FreeRTOS_recvfrom is static
+ * memory */
+void FreeRTOS_ReleaseUDPPayloadBuffer( void * pvBuffer )
+{
+    __CPROVER_assert( pvBuffer != NULL,
+                      "FreeRTOS precondition: pvBuffer != NULL" );
+}
+
 /****************************************************************
 * Abstract DNS_ParseDNSReply proved memory safe in ParseDNSReply.
 *
@@ -122,20 +172,39 @@ BaseType_t DNS_ReadReply( ConstSocket_t xDNSSocket,
                           struct freertos_sockaddr * xAddress,
                           struct xDNSBuffer * pxDNSBuf )
 {
-    BaseType_t ret;
     int len;
+    uintptr_t uxTypeOffset;
+    const uint8_t * pucIPType;
+    uint8_t ucIPType;
+    NetworkBufferDescriptor_t * pxNetworkEndPoints;
 
-    __CPROVER_assume( ( len > sizeof( DNSMessage_t ) ) && ( len < CBMC_MAX_OBJECT_SIZE ) );
+    __CPROVER_assume( ( len > sizeof( DNSMessage_t ) ) && ( len < ipconfigNETWORK_MTU ) );
 
-    pxDNSBuf->pucPayloadBuffer = malloc( len );
+    pxNetworkEndPoints = pxGetNetworkBufferWithDescriptor( len, 0 );
+    __CPROVER_assume( pxNetworkEndPoints != NULL );
+    __CPROVER_assume( pxNetworkEndPoints->pucEthernetBuffer != NULL );
 
+    pxDNSBuf->pucPayloadBuffer = pxNetworkEndPoints->pucEthernetBuffer;
     pxDNSBuf->uxPayloadLength = len;
 
-    __CPROVER_assume( pxDNSBuf->pucPayloadBuffer != NULL );
-
     __CPROVER_havoc_slice( pxDNSBuf->pucPayloadBuffer, pxDNSBuf->uxPayloadLength );
 
-    return ret;
+    /* When IPv6 is supported, find out the type of the packet.
+     * It is stored 48 bytes before the payload buffer as 0x40 or 0x60. */
+    uxTypeOffset = __CPROVER_file_local_FreeRTOS_IP_Utils_c_void_ptr_to_uintptr( pxDNSBuf->pucPayloadBuffer );
+    uxTypeOffset -= ipUDP_PAYLOAD_IP_TYPE_OFFSET;
+    pucIPType = ( const uint8_t * ) uxTypeOffset;
+
+    /* For an IPv4 packet, pucIPType points to 6 bytes before the pucEthernetBuffer,
+     * for a IPv6 packet, pucIPType will point to the first byte of the IP-header: 'ucVersionTrafficClass'. */
+    ucIPType = pucIPType[ 0 ] & 0xf0U;
+
+    /* To help the translation from a UDP payload pointer to a networkBuffer,
+     * a byte was stored at a certain negative offset (-48 bytes).
+     * It must have a value of either 0x4x or 0x6x. */
+    __CPROVER_assume( ( ucIPType == ipTYPE_IPv4 ) || ( ucIPType == ipTYPE_IPv6 ) );
+
+    return nondet_basetype();
 }
 
 
@@ -193,54 +262,6 @@ size_t __CPROVER_file_local_FreeRTOS_DNS_c_prvCreateDNSMessage( uint8_t * pucUDP
     return size;
 }
 
-/*We assume that the pxGetNetworkBufferWithDescriptor function is implemented correctly and returns a valid data structure. */
-/*This is the mock to mimic the correct expected behavior. If this allocation fails, this might invalidate the proof. */
-NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes,
-                                                              TickType_t xBlockTimeTicks )
-{
-    NetworkBufferDescriptor_t * pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
-
-    if( pxNetworkBuffer != NULL )
-    {
-        pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xRequestedSizeBytes + ipUDP_PAYLOAD_IP_TYPE_OFFSET );
-
-        if( pxNetworkBuffer->pucEthernetBuffer == NULL )
-        {
-            free( pxNetworkBuffer );
-            pxNetworkBuffer = NULL;
-        }
-        else
-        {
-            pxNetworkBuffer->pucEthernetBuffer = ( ( uint8_t * ) pxNetworkBuffer->pucEthernetBuffer ) + ipUDP_PAYLOAD_IP_TYPE_OFFSET;
-            pxNetworkBuffer->xDataLength = xRequestedSizeBytes;
-        }
-    }
-
-    return pxNetworkBuffer;
-}
-
-/*
- * In this function, it only allocates network buffer by pxGetNetworkBufferWithDescriptor
- * stub function above here. In this case, we should free both network buffer descriptor and pucEthernetBuffer.
- */
-void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer )
-{
-    __CPROVER_assert( pxNetworkBuffer != NULL,
-                      "Precondition: pxNetworkBuffer != NULL" );
-
-    free( pxNetworkBuffer->pucEthernetBuffer - ipUDP_PAYLOAD_IP_TYPE_OFFSET );
-    free( pxNetworkBuffer );
-}
-
-/* FreeRTOS_ReleaseUDPPayloadBuffer is mocked here and the memory
- * is not freed as the buffer allocated by the FreeRTOS_recvfrom is static
- * memory */
-void FreeRTOS_ReleaseUDPPayloadBuffer( void * pvBuffer )
-{
-    __CPROVER_assert( pvBuffer != NULL,
-                      "FreeRTOS precondition: pvBuffer != NULL" );
-}
-
 uint32_t Prepare_CacheLookup( const char * pcHostName,
                               BaseType_t xFamily,
                               struct freertos_addrinfo ** ppxAddressInfo )
diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json
index 6df4759db..46a0c62cf 100644
--- a/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json
+++ b/test/cbmc/proofs/DNS/DNSgetHostByName/Makefile.json
@@ -31,7 +31,7 @@
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto",
diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c b/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c
index bcef7792b..03d1ecb73 100644
--- a/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c
+++ b/test/cbmc/proofs/DNS/DNSgetHostByName_a/DNSgetHostByName_a_harness.c
@@ -17,8 +17,11 @@
 #include "NetworkBufferManagement.h"
 #include "NetworkInterface.h"
 
+/* CBMC includes. */
 #include "cbmc.h"
 
+uintptr_t __CPROVER_file_local_FreeRTOS_IP_Utils_c_void_ptr_to_uintptr( const void * pvPointer );
+
 /****************************************************************
 * We abstract:
 *
@@ -37,6 +40,54 @@
 * bound the iterations of strcmp.
 ****************************************************************/
 
+/*We assume that the pxGetNetworkBufferWithDescriptor function is implemented correctly and returns a valid data structure. */
+/*This is the mock to mimic the correct expected behavior. If this allocation fails, this might invalidate the proof. */
+NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes,
+                                                              TickType_t xBlockTimeTicks )
+{
+    NetworkBufferDescriptor_t * pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
+
+    if( pxNetworkBuffer != NULL )
+    {
+        pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xRequestedSizeBytes + ipBUFFER_PADDING + ipUDP_PAYLOAD_IP_TYPE_OFFSET );
+
+        if( pxNetworkBuffer->pucEthernetBuffer == NULL )
+        {
+            free( pxNetworkBuffer );
+            pxNetworkBuffer = NULL;
+        }
+        else
+        {
+            pxNetworkBuffer->pucEthernetBuffer = ( ( uint8_t * ) pxNetworkBuffer->pucEthernetBuffer ) + ipBUFFER_PADDING + ipUDP_PAYLOAD_IP_TYPE_OFFSET;
+            pxNetworkBuffer->xDataLength = xRequestedSizeBytes;
+        }
+    }
+
+    return pxNetworkBuffer;
+}
+
+/*
+ * In this function, it only allocates network buffer by pxGetNetworkBufferWithDescriptor
+ * stub function above here. In this case, we should free both network buffer descriptor and pucEthernetBuffer.
+ */
+void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer )
+{
+    __CPROVER_assert( pxNetworkBuffer != NULL,
+                      "Precondition: pxNetworkBuffer != NULL" );
+
+    free( pxNetworkBuffer->pucEthernetBuffer - ( ipUDP_PAYLOAD_IP_TYPE_OFFSET + ipBUFFER_PADDING ) );
+    free( pxNetworkBuffer );
+}
+
+/* FreeRTOS_ReleaseUDPPayloadBuffer is mocked here and the memory
+ * is not freed as the buffer allocated by the FreeRTOS_recvfrom is static
+ * memory */
+void FreeRTOS_ReleaseUDPPayloadBuffer( void * pvBuffer )
+{
+    __CPROVER_assert( pvBuffer != NULL,
+                      "FreeRTOS precondition: pvBuffer != NULL" );
+}
+
 /****************************************************************
 * Abstract DNS_ParseDNSReply proved memory safe in ParseDNSReply.
 *
@@ -111,45 +162,6 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes
     return ret;
 }
 
-/*We assume that the pxGetNetworkBufferWithDescriptor function is implemented correctly and returns a valid data structure. */
-/*This is the mock to mimic the correct expected behavior. If this allocation fails, this might invalidate the proof. */
-NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes,
-                                                              TickType_t xBlockTimeTicks )
-{
-    NetworkBufferDescriptor_t * pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
-
-    if( pxNetworkBuffer != NULL )
-    {
-        pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xRequestedSizeBytes + ipBUFFER_PADDING + ipUDP_PAYLOAD_IP_TYPE_OFFSET );
-
-        if( pxNetworkBuffer->pucEthernetBuffer == NULL )
-        {
-            free( pxNetworkBuffer );
-            pxNetworkBuffer = NULL;
-        }
-        else
-        {
-            pxNetworkBuffer->pucEthernetBuffer = ( ( uint8_t * ) pxNetworkBuffer->pucEthernetBuffer ) + ipBUFFER_PADDING + ipUDP_PAYLOAD_IP_TYPE_OFFSET;
-            pxNetworkBuffer->xDataLength = xRequestedSizeBytes;
-        }
-    }
-
-    return pxNetworkBuffer;
-}
-
-/*
- * In this function, it only allocates network buffer by pxGetNetworkBufferWithDescriptor
- * stub function above here. In this case, we should free both network buffer descriptor and pucEthernetBuffer.
- */
-void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer )
-{
-    __CPROVER_assert( pxNetworkBuffer != NULL,
-                      "Precondition: pxNetworkBuffer != NULL" );
-
-    free( pxNetworkBuffer->pucEthernetBuffer - ( ipUDP_PAYLOAD_IP_TYPE_OFFSET + ipBUFFER_PADDING ) );
-    free( pxNetworkBuffer );
-}
-
 Socket_t DNS_CreateSocket( TickType_t uxReadTimeout_ticks )
 {
     Socket_t xSock = safeMalloc( sizeof( struct xSOCKET ) );
@@ -207,31 +219,21 @@ BaseType_t DNS_ReadReply( ConstSocket_t xDNSSocket,
                           struct freertos_sockaddr * xAddress,
                           struct xDNSBuffer * pxDNSBuf )
 {
-    BaseType_t ret;
     int len;
     NetworkBufferDescriptor_t * pxNetworkBuffer;
 
     __CPROVER_assume( ( len > sizeof( DNSMessage_t ) ) && ( len < ipconfigNETWORK_MTU ) );
 
-    if( nondet_bool() )
-    {
-        pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( len, 0 );
-        __CPROVER_assume( pxNetworkBuffer != NULL );
+    pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( len, 0 );
+    __CPROVER_assume( pxNetworkBuffer != NULL );
+    __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
 
-        pxDNSBuf->pucPayloadBuffer = pxNetworkBuffer->pucEthernetBuffer;
-        pxDNSBuf->uxPayloadLength = len;
-        __CPROVER_assume( pxDNSBuf->pucPayloadBuffer != NULL );
+    pxDNSBuf->pucPayloadBuffer = pxNetworkBuffer->pucEthernetBuffer;
+    pxDNSBuf->uxPayloadLength = len;
 
-        __CPROVER_havoc_slice( pxDNSBuf->pucPayloadBuffer, pxDNSBuf->uxPayloadLength );
+    __CPROVER_havoc_slice( pxDNSBuf->pucPayloadBuffer, pxDNSBuf->uxPayloadLength );
 
-        ret = len;
-    }
-    else
-    {
-        __CPROVER_assume( ret < 0 );
-    }
-
-    return ret;
+    return nondet_basetype();
 }
 
 /* Function xDNSSetCallBack is proven to be correct separately. */
diff --git a/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json b/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json
index 4f9571a34..e4114a1a6 100644
--- a/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json
+++ b/test/cbmc/proofs/DNS/DNSgetHostByName_a/Makefile.json
@@ -27,7 +27,6 @@
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_DNS_Parser.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP_Utils.goto",
     "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/cbmc.goto",
     "$(FREERTOS_PLUS_TCP)/test/cbmc/stubs/freertos_api.goto"