From 75e6fdec489c2592ea170c9d2c1f13cb545cca1e Mon Sep 17 00:00:00 2001
From: Kareem Khazem <karkhaz@amazon.com>
Date: Fri, 13 Jan 2023 17:42:24 +0000
Subject: [PATCH 01/28] Use CBMC XML output to enable VSCode debugger (#673)

Prior to this commit, CBMC would emit logging information in plain text
format, which does not contain information required for the CBMC VSCode
debugger. This commit makes CBMC use XML instead of plain text.

Co-authored-by: Mark Tuttle <tuttle@acm.org>
---
 test/cbmc/proofs/Makefile.template | 26 ++++++++++++--------------
 1 file changed, 12 insertions(+), 14 deletions(-)

diff --git a/test/cbmc/proofs/Makefile.template b/test/cbmc/proofs/Makefile.template
index 375c15c120..094fd560c1 100644
--- a/test/cbmc/proofs/Makefile.template
+++ b/test/cbmc/proofs/Makefile.template
@@ -119,8 +119,8 @@ goto:
 # Ignore the return code for CBMC, so that we can still generate the
 # report if the proof failed. If the proof failed, we separately fail
 # the entire job using the check-cbmc-result rule.
-cbmc.txt: $(ENTRY).goto
-	-cbmc $(CBMCFLAGS) $(SOLVER) --unwinding-assertions --trace @RULE_INPUT@ > $@ 2>&1
+cbmc.xml: $(ENTRY).goto
+	-cbmc $(CBMCFLAGS) $(SOLVER) --unwinding-assertions --trace --xml-ui @RULE_INPUT@ > $@ 2>&1
 
 property.xml: $(ENTRY).goto
 	cbmc $(CBMCFLAGS) --unwinding-assertions --show-properties --xml-ui @RULE_INPUT@ > $@ 2>&1
@@ -128,29 +128,27 @@ property.xml: $(ENTRY).goto
 coverage.xml: $(ENTRY).goto
 	cbmc $(CBMCFLAGS) --cover location --xml-ui @RULE_INPUT@ > $@ 2>&1
 
-cbmc: cbmc.txt
+cbmc: cbmc.xml
 
 property: property.xml
 
 coverage: coverage.xml
 
-report: cbmc.txt property.xml coverage.xml
+report: cbmc.xml property.xml coverage.xml
 	$(VIEWER) \
 	--goto $(ENTRY).goto \
 	--srcdir $(FREERTOS_PLUS_TCP) \
-	--blddir $(FREERTOS_PLUS_TCP) \
-	--htmldir html \
-	--srcexclude "(.@FORWARD_SLASH@doc|.@FORWARD_SLASH@tests|.@FORWARD_SLASH@vendors)" \
-	--result cbmc.txt \
+	--reportdir report \
+	--result cbmc.xml \
 	--property property.xml \
-	--block coverage.xml
+	--coverage coverage.xml
 
-# This rule depends only on cbmc.txt and has no dependents, so it will
+# This rule depends only on cbmc.xml and has no dependents, so it will
 # not block the report from being generated if it fails. This rule is
 # intended to fail if and only if the CBMC safety check that emits
-# cbmc.txt yielded a proof failure.
-check-cbmc-result: cbmc.txt
-	grep -e "^VERIFICATION SUCCESSFUL" $^
+# cbmc.xml yielded a proof failure.
+check-cbmc-result: cbmc.xml
+	grep '<cprover-status>SUCCESS</cprover-status>' $^
 
 # ____________________________________________________________________
 # Rules
@@ -160,7 +158,7 @@ check-cbmc-result: cbmc.txt
 clean:
 	@RM@ $(OBJS) $(ENTRY).goto
 	@RM@ $(ENTRY)[0-9].goto $(ENTRY)[0-9].txt
-	@RM@ cbmc.txt property.xml coverage.xml TAGS TAGS-*
+	@RM@ cbmc.xml property.xml coverage.xml TAGS TAGS-*
 	@RM@ *~ \#*
 	@RM@ queue_datastructure.h
 

From 5a0bac2bba9601100f988d477170c49b6e9948e2 Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Mon, 6 Feb 2023 09:42:26 +0000
Subject: [PATCH 02/28] Fixes CBMC proof for the ARPAgeCache function: * Adds
 /source/FreeRTOS_Routing.c to ARPAgeCache proof build * Assumes
 pxNetworkEndPoints and pxNetworkEndPoints->pxNetworkInterface are properly
 initialized before ARPAgeCache is used. * Assumes one endpoint and interface
 are only present

Changes to CBMC flags/configs:
* Added:
    * `--unwindset FreeRTOS_OutputARPRequest.0:3` and `--unwindset vARPAgeCache.1:3` as per number of endpoints
* Modified:
    * `--object-bits 8` to address: too many addressed objects: maximum number of objects is set to 2^n=128 (with n=7);
---
 test/cbmc/patches/FreeRTOSConfig.h            |  2 +-
 .../ARP/ARPAgeCache/ARPAgeCache_harness.c     | 28 +++++++++++++++++++
 .../cbmc/proofs/ARP/ARPAgeCache/Makefile.json |  3 ++
 test/cbmc/proofs/MakefileCommon.json          |  2 +-
 4 files changed, 33 insertions(+), 2 deletions(-)

diff --git a/test/cbmc/patches/FreeRTOSConfig.h b/test/cbmc/patches/FreeRTOSConfig.h
index e3ed1f8ad5..7e61af32f1 100644
--- a/test/cbmc/patches/FreeRTOSConfig.h
+++ b/test/cbmc/patches/FreeRTOSConfig.h
@@ -127,7 +127,7 @@
  * is set to 2 so the formatting functions are included without the stdio.h being
  * included in tasks.c.  That is because this project defines its own sprintf()
  * functions. */
-#define configUSE_STATS_FORMATTING_FUNCTIONS    1
+#define configUSE_STATS_FORMATTING_FUNCTIONS    0
 
 /* Assert call defined for debug builds. */
 extern void vAssertCalled( const char * pcFile,
diff --git a/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c b/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c
index d90f1c247a..70278bdaab 100644
--- a/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c
+++ b/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c
@@ -23,7 +23,35 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS
     return pxNetworkBuffer;
 }
 
+BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDescriptor,
+                                                NetworkBufferDescriptor_t * const pxNetworkBuffer,
+                                                BaseType_t xReleaseAfterSend )
+{
+    return 0;
+}
+
 void harness()
 {
+    /*
+    For this proof, its assumed that the endpoints and interfaces are correctly
+    initialised and the pointers are set correctly.
+    Assumes two endpoints and interface is present.
+    */
+
+    pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkEndPoints != NULL );
+    pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
+    __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNext == NULL );
+
+    /* Interface init. */
+    pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
+    __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
+    pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
+    __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNetworkInterface != NULL );
+
+    pxNetworkEndPoints->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub;
+    /* No assumption is added for pfOutput as its pointed to a static object/memory location. */
+    
     vARPAgeCache();
 }
diff --git a/test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json b/test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json
index 1358682d1a..0b59aa2e4c 100644
--- a/test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json
+++ b/test/cbmc/proofs/ARP/ARPAgeCache/Makefile.json
@@ -4,12 +4,15 @@
   [
       "--unwind 1",
       "--unwindset vARPAgeCache.0:7",
+      "--unwindset FreeRTOS_OutputARPRequest.0:3",
+      "--unwindset vARPAgeCache.1:3",
       "--nondet-static"
   ],
   "OBJS":
   [
     "$(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)/test/FreeRTOS-Kernel/tasks.goto"
   ],
diff --git a/test/cbmc/proofs/MakefileCommon.json b/test/cbmc/proofs/MakefileCommon.json
index ace4a5c352..7ada3e1dca 100644
--- a/test/cbmc/proofs/MakefileCommon.json
+++ b/test/cbmc/proofs/MakefileCommon.json
@@ -31,7 +31,7 @@
     ],
 
     "CBMCFLAGS ": [
-	"--object-bits 7",
+	"--object-bits 8",
 	"--32",
 	"--bounds-check",
 	"--pointer-check"

From a1371d954f2f3be0187cc3e80a93009ee4f0bd73 Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Mon, 6 Feb 2023 11:35:35 +0000
Subject: [PATCH 03/28] Fixes CBMC proof build failure and proof failure for
 ARP_FreeRTOS_ClearARP:

* New flags:
    * "--unwindset FreeRTOS_ClearARP.0:7" to support loop in cleararp function

* Added argument to FreeRTOS_ClearARP in harness to support new change in API
---
 .../proofs/ARP/ARP_FreeRTOS_ClearARP/ClearARP_harness.c  | 9 ++++++++-
 test/cbmc/proofs/ARP/ARP_FreeRTOS_ClearARP/Makefile.json | 3 ++-
 2 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/test/cbmc/proofs/ARP/ARP_FreeRTOS_ClearARP/ClearARP_harness.c b/test/cbmc/proofs/ARP/ARP_FreeRTOS_ClearARP/ClearARP_harness.c
index de16e8385f..75d2c3da09 100644
--- a/test/cbmc/proofs/ARP/ARP_FreeRTOS_ClearARP/ClearARP_harness.c
+++ b/test/cbmc/proofs/ARP/ARP_FreeRTOS_ClearARP/ClearARP_harness.c
@@ -8,5 +8,12 @@
 
 void harness()
 {
-    FreeRTOS_ClearARP();
+
+    NetworkEndPoint_t *pxEndPoint_Test = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    /*
+    Here the assumption that pxEndPoint_Test != NULL [__CPROVER_assume( pxEndPoint_Test != NULL );]
+    is not made as pxEndPoint_Test == NULL is a valid use case.
+    */
+
+    FreeRTOS_ClearARP(pxEndPoint_Test);
 }
diff --git a/test/cbmc/proofs/ARP/ARP_FreeRTOS_ClearARP/Makefile.json b/test/cbmc/proofs/ARP/ARP_FreeRTOS_ClearARP/Makefile.json
index 118d131547..515d802c7a 100644
--- a/test/cbmc/proofs/ARP/ARP_FreeRTOS_ClearARP/Makefile.json
+++ b/test/cbmc/proofs/ARP/ARP_FreeRTOS_ClearARP/Makefile.json
@@ -2,7 +2,8 @@
   "ENTRY": "ClearARP",
   "CBMCFLAGS":
   [
-      "--unwind 1"
+      "--unwind 1",
+      "--unwindset FreeRTOS_ClearARP.0:7"
   ],
   "OBJS":
   [

From ff05ea374af96adc1cf13436c4f1dadc735a54bc Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Tue, 7 Feb 2023 07:02:41 +0000
Subject: [PATCH 04/28] Fixed ARPGenerateRequestPacket CBMC proof

---
 .../ARPGenerateRequestPacket_harness.c                     | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/test/cbmc/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c b/test/cbmc/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c
index c949e10c26..d98e640469 100644
--- a/test/cbmc/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c
+++ b/test/cbmc/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c
@@ -26,6 +26,13 @@ void harness()
     xNetworkBuffer2.pucEthernetBuffer = xBuffer;
     xNetworkBuffer2.xDataLength = ucBUFFER_SIZE;
 
+    /*
+    This proof assumes one end point is present.
+    */
+    xNetworkBuffer2.pxEndPoint = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( xNetworkBuffer2.pxEndPoint != NULL );
+    __CPROVER_assume( xNetworkBuffer2.pxEndPoint->pxNext == NULL );
+
     /* vARPGenerateRequestPacket asserts buffer has room for a packet */
     __CPROVER_assume( xNetworkBuffer2.xDataLength >= sizeof( ARPPacket_t ) );
     vARPGenerateRequestPacket( &xNetworkBuffer2 );

From be35723636523c846e467de99f331b323323d0e6 Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Tue, 7 Feb 2023 10:29:59 +0000
Subject: [PATCH 05/28] Fixed ARPGetCacheEntryByMac proof:

Changes
-------
Removed --nondet-static: proof fails if that option is enabled as the endpoint gets random value even if there is NULL check before its usage
---
 .../ARPGetCacheEntryByMac_harness.c                | 14 +++++++++++++-
 .../proofs/ARP/ARPGetCacheEntryByMac/Makefile.json |  3 +--
 2 files changed, 14 insertions(+), 3 deletions(-)

diff --git a/test/cbmc/proofs/ARP/ARPGetCacheEntryByMac/ARPGetCacheEntryByMac_harness.c b/test/cbmc/proofs/ARP/ARPGetCacheEntryByMac/ARPGetCacheEntryByMac_harness.c
index 1a6f0daf59..f0c9ddcc6b 100644
--- a/test/cbmc/proofs/ARP/ARPGetCacheEntryByMac/ARPGetCacheEntryByMac_harness.c
+++ b/test/cbmc/proofs/ARP/ARPGetCacheEntryByMac/ARPGetCacheEntryByMac_harness.c
@@ -7,10 +7,22 @@
 #include "FreeRTOS_IP_Private.h"
 #include "FreeRTOS_ARP.h"
 
+extern ARPCacheRow_t xARPCache[ ipconfigARP_CACHE_ENTRIES ];
+
+static NetworkEndPoint_t xEndPoint_Temp;
+
 void harness()
 {
     MACAddress_t xMACAddress;
     uint32_t ulIPAddress;
 
-    eARPGetCacheEntryByMac( &xMACAddress, &ulIPAddress );
+    NetworkInterface_t **ppxInterface = ( NetworkInterface_t ** ) malloc( sizeof( NetworkInterface_t * ) );
+
+    if ( ppxInterface )
+    {
+        *ppxInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
+        __CPROVER_assume( *ppxInterface != NULL );
+    }
+    
+    eARPGetCacheEntryByMac( &xMACAddress, &ulIPAddress, ppxInterface );
 }
diff --git a/test/cbmc/proofs/ARP/ARPGetCacheEntryByMac/Makefile.json b/test/cbmc/proofs/ARP/ARPGetCacheEntryByMac/Makefile.json
index a688d62dec..05839a9ef6 100644
--- a/test/cbmc/proofs/ARP/ARPGetCacheEntryByMac/Makefile.json
+++ b/test/cbmc/proofs/ARP/ARPGetCacheEntryByMac/Makefile.json
@@ -2,8 +2,7 @@
   "ENTRY": "ARPGetCacheEntryByMac",
   "CBMCFLAGS":
   [
-      "--unwind 7",
-      "--nondet-static"
+      "--unwind 7"
   ],
   "OBJS":
   [

From 441e26687934be891043ffb19437b2ed9a883ba3 Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Tue, 7 Feb 2023 11:48:35 +0000
Subject: [PATCH 06/28] Fix ARPProcessPacket CBMC proof:

Changes:
-------
ARPProcessPacket takes new arg (NetworkBufferDescriptor_t *)
---
 .../ARPProcessPacket_harness.c                | 27 +++++++++++++++++--
 .../proofs/ARP/ARPProcessPacket/Makefile.json |  1 +
 2 files changed, 26 insertions(+), 2 deletions(-)

diff --git a/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c b/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
index 33e60182a7..762bb1e238 100644
--- a/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
+++ b/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
@@ -17,7 +17,6 @@ void FreeRTOS_OutputARPRequest( uint32_t ulIPAddress )
 
 void harness()
 {
-    ARPPacket_t xARPFrame;
     NetworkBufferDescriptor_t xLocalBuffer;
     uint16_t usEthernetBufferSize;
 
@@ -47,5 +46,29 @@ void harness()
         pxARPWaitingNetworkBuffer = NULL;
     }
 
-    eARPProcessPacket( &xARPFrame );
+    /*
+     * The assumption made here is that the buffer pointed by pucEthernetBuffer
+     * is at least allocated to sizeof(ARPPacket_t) size but eventually a even larger buffer.
+     * This is not checked inside eARPProcessPacket.
+     */
+    uint8_t ucBUFFER_SIZE;
+
+    __CPROVER_assume( ucBUFFER_SIZE >= sizeof( ARPPacket_t ) && ucBUFFER_SIZE < 2 * sizeof( ARPPacket_t ) );
+    void * xBuffer = malloc( ucBUFFER_SIZE );
+
+    __CPROVER_assume( xBuffer != NULL );
+
+    NetworkBufferDescriptor_t xNetworkBuffer2;
+
+    xNetworkBuffer2.pucEthernetBuffer = xBuffer;
+    xNetworkBuffer2.xDataLength = ucBUFFER_SIZE;
+
+    /*
+    This proof assumes one end point is present.
+    */
+    xNetworkBuffer2.pxEndPoint = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( xNetworkBuffer2.pxEndPoint != NULL );
+    __CPROVER_assume( xNetworkBuffer2.pxEndPoint->pxNext == NULL );
+
+    eARPProcessPacket( &xNetworkBuffer2 );
 }
diff --git a/test/cbmc/proofs/ARP/ARPProcessPacket/Makefile.json b/test/cbmc/proofs/ARP/ARPProcessPacket/Makefile.json
index 9cfdef0d0e..177967c132 100644
--- a/test/cbmc/proofs/ARP/ARPProcessPacket/Makefile.json
+++ b/test/cbmc/proofs/ARP/ARPProcessPacket/Makefile.json
@@ -4,6 +4,7 @@
   [
       "--unwind 1",
       "--unwindset vARPRefreshCacheEntry.0:7,memcmp.0:17,xIsIPInARPCache.0:7",
+      "--unwindset prvFindCacheEntry.0:7", 
       "--nondet-static"
   ],
   "OBJS":

From 19996391df6b973fb5d44a9710e2034d0665dc44 Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Tue, 7 Feb 2023 16:45:58 +0000
Subject: [PATCH 07/28] Fixed CBMC proof for ARP_OutputARPRequest_buffer_alloc1
 diff configs

---
 .../Configurations.json                       |  1 +
 .../OutputARPRequest_harness.c                | 27 ++++++++++++++++---
 2 files changed, 24 insertions(+), 4 deletions(-)

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 44b83cb2cc..e243382c31 100644
--- a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json
+++ b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc1/Configurations.json
@@ -11,6 +11,7 @@
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto",
+    "$(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"
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 f4c510ac0a..944b9f09b0 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
@@ -61,19 +61,38 @@ void * pvPortMalloc( size_t xWantedSize )
  * for releasing the buffer to the end. Apart from that, it is up to the vendor,
  * how to write this code out to the network.
  */
-BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxDescriptor,
-                                    BaseType_t bReleaseAfterSend )
+BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDescriptor,
+                                                NetworkBufferDescriptor_t * const pxNetworkBuffer,
+                                                BaseType_t xReleaseAfterSend )
 {
-    if( bReleaseAfterSend != pdFALSE )
+    if( xReleaseAfterSend != pdFALSE )
     {
-        vReleaseNetworkBufferAndDescriptor( pxDescriptor );
+        vReleaseNetworkBufferAndDescriptor( pxNetworkBuffer );
     }
 }
 
+
 void harness()
 {
     BaseType_t xRes = xNetworkBuffersInitialise();
 
+    /*
+    For this proof, its assumed that the endpoints and interfaces are correctly
+    initialised and the pointers are set correctly.
+    Assumes two endpoints and interface is present.
+    */
+
+    pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkEndPoints != NULL );
+    __CPROVER_assume( pxNetworkEndPoints->pxNext == NULL );
+
+    /* Interface init. */
+    pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
+    __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
+
+    pxNetworkEndPoints->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub;
+    /* No assumption is added for pfOutput as its pointed to a static object/memory location. */
+
     if( xRes == pdPASS )
     {
         uint32_t ulIPAddress;

From e0f3d752e6a5645d6fc91f982a81f66c2c6cbb45 Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Tue, 7 Feb 2023 16:54:02 +0000
Subject: [PATCH 08/28] Fixed CBMC proof for ARP_OutputARPRequest_buffer_alloc2
 diff configs

---
 .../Configurations.json                       |  1 +
 .../OutputARPRequest_harness.c                | 26 ++++++++++++++++---
 2 files changed, 23 insertions(+), 4 deletions(-)

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 6095add00a..5b2cdd30db 100644
--- a/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json
+++ b/test/cbmc/proofs/ARP/ARP_OutputARPRequest_buffer_alloc2/Configurations.json
@@ -11,6 +11,7 @@
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
+    "$(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"
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 775ae39ae2..1683553abd 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
@@ -41,12 +41,13 @@ void vPortFree( void * pv )
  * This function function writes a buffer to the network.  We stub it
  * out here, and assume it has no side effects relevant to memory safety.
  */
-BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxDescriptor,
-                                    BaseType_t bReleaseAfterSend )
+BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDescriptor,
+                                                NetworkBufferDescriptor_t * const pxNetworkBuffer,
+                                                BaseType_t xReleaseAfterSend )
 {
-    if( bReleaseAfterSend != pdFALSE )
+    if( xReleaseAfterSend != pdFALSE )
     {
-        vReleaseNetworkBufferAndDescriptor( pxDescriptor );
+        vReleaseNetworkBufferAndDescriptor( pxNetworkBuffer );
     }
 }
 
@@ -54,6 +55,23 @@ void harness()
 {
     BaseType_t xRes = xNetworkBuffersInitialise();
 
+    /*
+    For this proof, its assumed that the endpoints and interfaces are correctly
+    initialised and the pointers are set correctly.
+    Assumes two endpoints and interface is present.
+    */
+
+    pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkEndPoints != NULL );
+    __CPROVER_assume( pxNetworkEndPoints->pxNext == NULL );
+
+    /* Interface init. */
+    pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
+    __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
+
+    pxNetworkEndPoints->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub;
+    /* No assumption is added for pfOutput as its pointed to a static object/memory location. */
+
     if( xRes == pdPASS )
     {
         uint32_t ulIPAddress;

From c17d11debc28716cc24223c623efc460ab3e417f Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Tue, 7 Feb 2023 18:11:37 +0000
Subject: [PATCH 09/28] Fix CBMC proof for ARPGetCacheEntry

---
 .../ARPGetCacheEntry_harness.c                | 24 ++++++++++++++++++-
 .../ARP/ARPGetCacheEntry/Configurations.json  |  5 ++++
 .../OutputARPRequest_harness.c                |  2 +-
 .../OutputARPRequest_harness.c                |  2 +-
 4 files changed, 30 insertions(+), 3 deletions(-)

diff --git a/test/cbmc/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c b/test/cbmc/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c
index 1a47e8e971..1921a239ae 100644
--- a/test/cbmc/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c
+++ b/test/cbmc/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c
@@ -13,5 +13,27 @@ void harness()
     uint32_t ulIPAddress;
     MACAddress_t xMACAddress;
 
-    eARPGetCacheEntry( &ulIPAddress, &xMACAddress );
+    /*
+    For this proof, its assumed that the endpoints and interfaces are correctly
+    initialised and the pointers are set correctly.
+    Assumes one endpoint and interface is present.
+    */
+
+    pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkEndPoints != NULL );
+    __CPROVER_assume( pxNetworkEndPoints->pxNext == NULL );
+
+    /* Interface init. */
+    pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
+    __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
+
+    NetworkInterface_t **ppxInterface = ( NetworkInterface_t ** ) malloc( sizeof( NetworkInterface_t * ) );
+
+    if ( ppxInterface )
+    {
+        *ppxInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
+        __CPROVER_assume( *ppxInterface != NULL );
+    }
+
+    eARPGetCacheEntry( &ulIPAddress, &xMACAddress, ppxInterface );
 }
diff --git a/test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json b/test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json
index 8309f49c80..0346767246 100644
--- a/test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json
+++ b/test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json
@@ -4,11 +4,16 @@
   [
       "--unwind 1",
       "--unwindset prvCacheLookup.0:7",
+      "--unwindset FreeRTOS_FindEndPointOnIP_IPv4.0:2",
+      "--unwindset FreeRTOS_InterfaceEndPointOnNetMask.0:2",
+      "--unwindset eARPGetCacheEntry.0:2",
+      "--unwindset FreeRTOS_FindGateWay.0:2",
       "--nondet-static"
   ],
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.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 944b9f09b0..79d6cad90c 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
@@ -79,7 +79,7 @@ void harness()
     /*
     For this proof, its assumed that the endpoints and interfaces are correctly
     initialised and the pointers are set correctly.
-    Assumes two endpoints and interface is present.
+    Assumes one endpoint and interface is present.
     */
 
     pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
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 1683553abd..38f54b2494 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
@@ -58,7 +58,7 @@ void harness()
     /*
     For this proof, its assumed that the endpoints and interfaces are correctly
     initialised and the pointers are set correctly.
-    Assumes two endpoints and interface is present.
+    Assumes one endpoint and interface is present.
     */
 
     pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );

From 759182e00d674f2baaa6856612ffef5085e8310c Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Wed, 8 Feb 2023 04:38:54 +0000
Subject: [PATCH 10/28] Fixed proofs for ARPRefreshCacheEntry

---
 .../ARPRefreshCacheEntry_harness.c              | 17 +++++++++++++++--
 .../ARPRefreshCacheEntry/Configurations.json    |  7 ++++---
 2 files changed, 19 insertions(+), 5 deletions(-)

diff --git a/test/cbmc/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c b/test/cbmc/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c
index 6c9a15ba28..a4919392a9 100644
--- a/test/cbmc/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c
+++ b/test/cbmc/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c
@@ -11,6 +11,19 @@ void harness()
     MACAddress_t xMACAddress;
     uint32_t ulIPAddress;
 
-    vARPRefreshCacheEntry( &xMACAddress, ulIPAddress );
-    vARPRefreshCacheEntry( NULL, ulIPAddress );
+    /*
+    For this proof, its assumed that the endpoints and interfaces are correctly
+    initialised and the pointers are set correctly.
+    Assumes one endpoints and interface is present.
+    */
+
+    pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkEndPoints != NULL );
+    __CPROVER_assume( pxNetworkEndPoints->pxNext == NULL );
+
+    NetworkEndPoint_t * pxEndPoint = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxEndPoint != NULL );
+
+    vARPRefreshCacheEntry( &xMACAddress, ulIPAddress, pxEndPoint );
+    vARPRefreshCacheEntry( NULL, ulIPAddress, pxEndPoint );
 }
diff --git a/test/cbmc/proofs/ARP/ARPRefreshCacheEntry/Configurations.json b/test/cbmc/proofs/ARP/ARPRefreshCacheEntry/Configurations.json
index cd2f75bac5..143f22c1e0 100644
--- a/test/cbmc/proofs/ARP/ARPRefreshCacheEntry/Configurations.json
+++ b/test/cbmc/proofs/ARP/ARPRefreshCacheEntry/Configurations.json
@@ -3,13 +3,14 @@
   "CBMCFLAGS":
   [
       "--unwind 1",
-      "--unwindset vARPRefreshCacheEntry.0:7,memcmp.0:17",
-      "--nondet-static"
+      "--unwindset FreeRTOS_InterfaceEndPointOnNetMask.0:2",
+      "--unwindset prvFindCacheEntry.0:7,memcmp.0:17"
   ],
   "OBJS":
   [
     "$(ENTRY)_harness.goto",
-    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto"
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto"
   ],
   "DEF":
   [

From 2895b315ca7cd13f11d2143849656f9fc9a9447d Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Wed, 8 Feb 2023 05:12:56 +0000
Subject: [PATCH 11/28] Fixed CBMC proof for ARP_FreeRTOS_OutputARPRequest

---
 .../Configurations.json                       |  1 +
 .../OutputARPRequest_harness.c                | 24 +++++++++++++++++++
 2 files changed, 25 insertions(+)

diff --git a/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json b/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json
index 0abf4b47d6..62bb3e0523 100644
--- a/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json
+++ b/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/Configurations.json
@@ -36,6 +36,7 @@
   [
     "$(ENTRY)_harness.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_IP.goto",
+    "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_Routing.goto",
     "$(FREERTOS_PLUS_TCP)/source/FreeRTOS_ARP.goto"
   ],
   #That is the minimal required size for an ARPPacket_t plus offset in the buffer.
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 b21faeb422..11d12d9797 100644
--- a/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c
+++ b/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c
@@ -72,10 +72,34 @@ NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedS
     return &xNetworkBuffer;
 }
 
+BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDescriptor,
+                                                NetworkBufferDescriptor_t * const pxNetworkBuffer,
+                                                BaseType_t xReleaseAfterSend )
+{
+
+}
+
 
 void harness()
 {
     uint32_t ulIPAddress;
 
+    /*
+    For this proof, its assumed that the endpoints and interfaces are correctly
+    initialised and the pointers are set correctly.
+    Assumes one endpoint and interface is present.
+    */
+
+    pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkEndPoints != NULL );
+    __CPROVER_assume( pxNetworkEndPoints->pxNext == NULL );
+
+    /* Interface init. */
+    pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
+    __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
+
+    pxNetworkEndPoints->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub;
+    /* No assumption is added for pfOutput as its pointed to a static object/memory location. */
+
     FreeRTOS_OutputARPRequest( ulIPAddress );
 }

From a5d9b5717b0bd5689db71df58ef9f032184ed17d Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Sat, 11 Feb 2023 09:35:48 +0000
Subject: [PATCH 12/28] Fix cbmc proof for ARPProcessPacket

---
 .../ARP/ARPProcessPacket/ARPProcessPacket_harness.c       | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c b/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
index 762bb1e238..3342e40ddc 100644
--- a/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
+++ b/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
@@ -1,3 +1,5 @@
+#include "cbmc.h"
+
 /* FreeRTOS includes. */
 #include "FreeRTOS.h"
 #include "queue.h"
@@ -53,15 +55,15 @@ void harness()
      */
     uint8_t ucBUFFER_SIZE;
 
-    __CPROVER_assume( ucBUFFER_SIZE >= sizeof( ARPPacket_t ) && ucBUFFER_SIZE < 2 * sizeof( ARPPacket_t ) );
-    void * xBuffer = malloc( ucBUFFER_SIZE );
+    __CPROVER_assume( ucBUFFER_SIZE < CBMC_MAX_OBJECT_SIZE );
+    void * xBuffer = malloc( ucBUFFER_SIZE + sizeof( ARPPacket_t ) );
 
     __CPROVER_assume( xBuffer != NULL );
 
     NetworkBufferDescriptor_t xNetworkBuffer2;
 
     xNetworkBuffer2.pucEthernetBuffer = xBuffer;
-    xNetworkBuffer2.xDataLength = ucBUFFER_SIZE;
+    xNetworkBuffer2.xDataLength = ucBUFFER_SIZE + sizeof(ARPPacket_t);
 
     /*
     This proof assumes one end point is present.

From a48c5ef46454c8542fb06b646004e6999970365c Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Mon, 13 Feb 2023 06:30:51 +0000
Subject: [PATCH 13/28] fixed cbmc target func not called issue in
 ARP_FreeRTOS_PrintARPCache

---
 .../FreeRTOS_PrintARPCache_harness.c                           | 2 ++
 test/cbmc/proofs/ARP/ARP_FreeRTOS_PrintARPCache/Makefile.json  | 3 ++-
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/test/cbmc/proofs/ARP/ARP_FreeRTOS_PrintARPCache/FreeRTOS_PrintARPCache_harness.c b/test/cbmc/proofs/ARP/ARP_FreeRTOS_PrintARPCache/FreeRTOS_PrintARPCache_harness.c
index b0224412c5..e14e97ff10 100644
--- a/test/cbmc/proofs/ARP/ARP_FreeRTOS_PrintARPCache/FreeRTOS_PrintARPCache_harness.c
+++ b/test/cbmc/proofs/ARP/ARP_FreeRTOS_PrintARPCache/FreeRTOS_PrintARPCache_harness.c
@@ -8,6 +8,8 @@
 #include "FreeRTOSIPConfig.h"
 #include "FreeRTOS_ARP.h"
 
+void FreeRTOS_PrintARPCache( void );
+
 void harness()
 {
     FreeRTOS_PrintARPCache();
diff --git a/test/cbmc/proofs/ARP/ARP_FreeRTOS_PrintARPCache/Makefile.json b/test/cbmc/proofs/ARP/ARP_FreeRTOS_PrintARPCache/Makefile.json
index 58c1d7b195..b5241063d8 100644
--- a/test/cbmc/proofs/ARP/ARP_FreeRTOS_PrintARPCache/Makefile.json
+++ b/test/cbmc/proofs/ARP/ARP_FreeRTOS_PrintARPCache/Makefile.json
@@ -12,6 +12,7 @@
   ],
   "DEF":
   [
-    "ipconfigARP_CACHE_ENTRIES=6"
+    "ipconfigARP_CACHE_ENTRIES=6",
+    "ipconfigHAS_PRINTF=1"
   ]
 }

From 62f06384a5aeea96844d9857220c3bc7d6fbbc57 Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Tue, 14 Feb 2023 10:41:19 +0000
Subject: [PATCH 14/28] adding changes as per review comments

---
 test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c        | 2 ++
 .../proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c    | 3 +--
 .../ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c  | 3 +++
 .../OutputARPRequest_harness.c                                | 4 ++++
 4 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c b/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c
index 70278bdaab..bca1c12fec 100644
--- a/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c
+++ b/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c
@@ -27,6 +27,8 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes
                                                 NetworkBufferDescriptor_t * const pxNetworkBuffer,
                                                 BaseType_t xReleaseAfterSend )
 {
+    __CPROVER_assert( pxDescriptor != NULL, "The network interface cannot be NULL." );
+    __CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." );
     return 0;
 }
 
diff --git a/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c b/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
index 3342e40ddc..f95627c9a9 100644
--- a/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
+++ b/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
@@ -50,12 +50,11 @@ void harness()
 
     /*
      * The assumption made here is that the buffer pointed by pucEthernetBuffer
-     * is at least allocated to sizeof(ARPPacket_t) size but eventually a even larger buffer.
+     * 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;
 
-    __CPROVER_assume( ucBUFFER_SIZE < CBMC_MAX_OBJECT_SIZE );
     void * xBuffer = malloc( ucBUFFER_SIZE + sizeof( ARPPacket_t ) );
 
     __CPROVER_assume( xBuffer != NULL );
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 11d12d9797..b8e52c1c23 100644
--- a/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c
+++ b/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c
@@ -77,6 +77,9 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes
                                                 BaseType_t xReleaseAfterSend )
 {
 
+    __CPROVER_assert( pxDescriptor != NULL, "The network interface cannot be NULL." );
+    __CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." );
+
 }
 
 
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 38f54b2494..1f77b87d83 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
@@ -45,6 +45,10 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes
                                                 NetworkBufferDescriptor_t * const pxNetworkBuffer,
                                                 BaseType_t xReleaseAfterSend )
 {
+
+    __CPROVER_assert( pxDescriptor != NULL, "The network interface cannot be NULL." );
+    __CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." );
+    
     if( xReleaseAfterSend != pdFALSE )
     {
         vReleaseNetworkBufferAndDescriptor( pxNetworkBuffer );

From 563b329c8c53c810aea3ae32f731ab4746fcd092 Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Tue, 14 Feb 2023 16:28:01 +0000
Subject: [PATCH 15/28] add multiple endpoints

---
 .../ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c   |  6 +++++-
 .../proofs/ARP/ARPGetCacheEntry/Configurations.json   |  8 ++++----
 .../ARPRefreshCacheEntry_harness.c                    | 11 ++++++++++-
 .../OutputARPRequest_harness.c                        |  6 +++++-
 .../OutputARPRequest_harness.c                        |  6 +++++-
 5 files changed, 29 insertions(+), 8 deletions(-)

diff --git a/test/cbmc/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c b/test/cbmc/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c
index 1921a239ae..bd7e4fc91b 100644
--- a/test/cbmc/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c
+++ b/test/cbmc/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c
@@ -21,11 +21,15 @@ void harness()
 
     pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
     __CPROVER_assume( pxNetworkEndPoints != NULL );
-    __CPROVER_assume( pxNetworkEndPoints->pxNext == NULL );
+    pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
+    __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNext == NULL );
 
     /* Interface init. */
     pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
     __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
+    pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
+    __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNetworkInterface != NULL );
 
     NetworkInterface_t **ppxInterface = ( NetworkInterface_t ** ) malloc( sizeof( NetworkInterface_t * ) );
 
diff --git a/test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json b/test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json
index 0346767246..aa4d602966 100644
--- a/test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json
+++ b/test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json
@@ -4,10 +4,10 @@
   [
       "--unwind 1",
       "--unwindset prvCacheLookup.0:7",
-      "--unwindset FreeRTOS_FindEndPointOnIP_IPv4.0:2",
-      "--unwindset FreeRTOS_InterfaceEndPointOnNetMask.0:2",
-      "--unwindset eARPGetCacheEntry.0:2",
-      "--unwindset FreeRTOS_FindGateWay.0:2",
+      "--unwindset FreeRTOS_FindEndPointOnIP_IPv4.0:3",
+      "--unwindset FreeRTOS_InterfaceEndPointOnNetMask.0:3",
+      "--unwindset eARPGetCacheEntry.0:3",
+      "--unwindset FreeRTOS_FindGateWay.0:3",
       "--nondet-static"
   ],
   "OBJS":
diff --git a/test/cbmc/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c b/test/cbmc/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c
index a4919392a9..f7bd265dfc 100644
--- a/test/cbmc/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c
+++ b/test/cbmc/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c
@@ -19,7 +19,16 @@ void harness()
 
     pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
     __CPROVER_assume( pxNetworkEndPoints != NULL );
-    __CPROVER_assume( pxNetworkEndPoints->pxNext == NULL );
+    pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
+    __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNext == NULL );
+
+    /* Interface init. */
+    pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
+    __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
+    pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
+    __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNetworkInterface != NULL );
+
 
     NetworkEndPoint_t * pxEndPoint = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
     __CPROVER_assume( pxEndPoint != NULL );
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 b8e52c1c23..897301023d 100644
--- a/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c
+++ b/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c
@@ -95,11 +95,15 @@ void harness()
 
     pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
     __CPROVER_assume( pxNetworkEndPoints != NULL );
-    __CPROVER_assume( pxNetworkEndPoints->pxNext == NULL );
+    pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
+    __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNext == NULL );
 
     /* Interface init. */
     pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
     __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
+    pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
+    __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNetworkInterface != NULL );
 
     pxNetworkEndPoints->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub;
     /* No assumption is added for pfOutput as its pointed to a static object/memory location. */
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 79d6cad90c..42af5b7c99 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
@@ -84,11 +84,15 @@ void harness()
 
     pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
     __CPROVER_assume( pxNetworkEndPoints != NULL );
-    __CPROVER_assume( pxNetworkEndPoints->pxNext == NULL );
+    pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+    __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
+    __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNext == NULL );
 
     /* Interface init. */
     pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
     __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
+    pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
+    __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNetworkInterface != NULL );
 
     pxNetworkEndPoints->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub;
     /* No assumption is added for pfOutput as its pointed to a static object/memory location. */

From 7b22b34f6694f525980c419b27a3b69e51560b1b Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Tue, 14 Feb 2023 17:16:07 +0000
Subject: [PATCH 16/28] config fix for multiple end point

---
 test/cbmc/proofs/ARP/ARPRefreshCacheEntry/Configurations.json | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/cbmc/proofs/ARP/ARPRefreshCacheEntry/Configurations.json b/test/cbmc/proofs/ARP/ARPRefreshCacheEntry/Configurations.json
index 143f22c1e0..d4b0af085c 100644
--- a/test/cbmc/proofs/ARP/ARPRefreshCacheEntry/Configurations.json
+++ b/test/cbmc/proofs/ARP/ARPRefreshCacheEntry/Configurations.json
@@ -3,7 +3,7 @@
   "CBMCFLAGS":
   [
       "--unwind 1",
-      "--unwindset FreeRTOS_InterfaceEndPointOnNetMask.0:2",
+      "--unwindset FreeRTOS_InterfaceEndPointOnNetMask.0:3",
       "--unwindset prvFindCacheEntry.0:7,memcmp.0:17"
   ],
   "OBJS":

From f575184e0f8d82f7b4023a177726fb65c4cf0f2d Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Tue, 14 Feb 2023 18:40:55 +0000
Subject: [PATCH 17/28] wip

---
 .../OutputARPRequest_harness.c                              | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

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 42af5b7c99..79d6cad90c 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
@@ -84,15 +84,11 @@ void harness()
 
     pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
     __CPROVER_assume( pxNetworkEndPoints != NULL );
-    pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
-    __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
-    __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNext == NULL );
+    __CPROVER_assume( pxNetworkEndPoints->pxNext == NULL );
 
     /* Interface init. */
     pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
     __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
-    pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
-    __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNetworkInterface != NULL );
 
     pxNetworkEndPoints->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub;
     /* No assumption is added for pfOutput as its pointed to a static object/memory location. */

From b6b388d9993eb51c3f83422b5e2bbe590c9d49ac Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Wed, 15 Feb 2023 23:29:51 +0530
Subject: [PATCH 18/28] assigning null instead of assuming

---
 test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c        | 4 ++--
 .../ARPGenerateRequestPacket_harness.c                        | 2 +-
 .../proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c    | 4 ++--
 .../ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c   | 4 ++--
 .../ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c  | 4 ++--
 .../OutputARPRequest_harness.c                                | 4 ++--
 .../OutputARPRequest_harness.c                                | 4 ++--
 7 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c b/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c
index bca1c12fec..39006e2f9c 100644
--- a/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c
+++ b/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c
@@ -44,13 +44,13 @@ void harness()
     __CPROVER_assume( pxNetworkEndPoints != NULL );
     pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
     __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
-    __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNext == NULL );
+    pxNetworkEndPoints->pxNext->pxNext = NULL;
 
     /* Interface init. */
     pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
     __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
     pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
-    __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNetworkInterface != NULL );
+    pxNetworkEndPoints->pxNext->pxNetworkInterface = NULL;
 
     pxNetworkEndPoints->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub;
     /* No assumption is added for pfOutput as its pointed to a static object/memory location. */
diff --git a/test/cbmc/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c b/test/cbmc/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c
index d98e640469..945e390525 100644
--- a/test/cbmc/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c
+++ b/test/cbmc/proofs/ARP/ARPGenerateRequestPacket/ARPGenerateRequestPacket_harness.c
@@ -31,7 +31,7 @@ void harness()
     */
     xNetworkBuffer2.pxEndPoint = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
     __CPROVER_assume( xNetworkBuffer2.pxEndPoint != NULL );
-    __CPROVER_assume( xNetworkBuffer2.pxEndPoint->pxNext == NULL );
+    xNetworkBuffer2.pxEndPoint->pxNext = NULL;
 
     /* vARPGenerateRequestPacket asserts buffer has room for a packet */
     __CPROVER_assume( xNetworkBuffer2.xDataLength >= sizeof( ARPPacket_t ) );
diff --git a/test/cbmc/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c b/test/cbmc/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c
index bd7e4fc91b..a845e9bb95 100644
--- a/test/cbmc/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c
+++ b/test/cbmc/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c
@@ -23,13 +23,13 @@ void harness()
     __CPROVER_assume( pxNetworkEndPoints != NULL );
     pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
     __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
-    __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNext == NULL );
+    pxNetworkEndPoints->pxNext->pxNext = NULL;
 
     /* Interface init. */
     pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
     __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
     pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
-    __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNetworkInterface != NULL );
+    pxNetworkEndPoints->pxNext->pxNetworkInterface = NULL;
 
     NetworkInterface_t **ppxInterface = ( NetworkInterface_t ** ) malloc( sizeof( NetworkInterface_t * ) );
 
diff --git a/test/cbmc/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c b/test/cbmc/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c
index f7bd265dfc..9b654e5fa9 100644
--- a/test/cbmc/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c
+++ b/test/cbmc/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c
@@ -21,13 +21,13 @@ void harness()
     __CPROVER_assume( pxNetworkEndPoints != NULL );
     pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
     __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
-    __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNext == NULL );
+    pxNetworkEndPoints->pxNext->pxNext = NULL;
 
     /* Interface init. */
     pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
     __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
     pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
-    __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNetworkInterface != NULL );
+    pxNetworkEndPoints->pxNext->pxNetworkInterface = NULL;
 
 
     NetworkEndPoint_t * pxEndPoint = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
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 897301023d..36a9487d09 100644
--- a/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c
+++ b/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c
@@ -97,13 +97,13 @@ void harness()
     __CPROVER_assume( pxNetworkEndPoints != NULL );
     pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
     __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
-    __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNext == NULL );
+    pxNetworkEndPoints->pxNext->pxNext = NULL;
 
     /* Interface init. */
     pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
     __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
     pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
-    __CPROVER_assume( pxNetworkEndPoints->pxNext->pxNetworkInterface != NULL );
+    pxNetworkEndPoints->pxNext->pxNetworkInterface = NULL;
 
     pxNetworkEndPoints->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub;
     /* No assumption is added for pfOutput as its pointed to a static object/memory location. */
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 79d6cad90c..c5eab45c5b 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
@@ -84,11 +84,11 @@ void harness()
 
     pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
     __CPROVER_assume( pxNetworkEndPoints != NULL );
-    __CPROVER_assume( pxNetworkEndPoints->pxNext == NULL );
+    pxNetworkEndPoints->pxNext = NULL;
 
     /* Interface init. */
     pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
-    __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
+    pxNetworkEndPoints->pxNetworkInterface = NULL;
 
     pxNetworkEndPoints->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub;
     /* No assumption is added for pfOutput as its pointed to a static object/memory location. */
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 1f77b87d83..d7fcc2aa28 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
@@ -67,11 +67,11 @@ void harness()
 
     pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
     __CPROVER_assume( pxNetworkEndPoints != NULL );
-    __CPROVER_assume( pxNetworkEndPoints->pxNext == NULL );
+    pxNetworkEndPoints->pxNext = NULL;
 
     /* Interface init. */
     pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
-    __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
+    pxNetworkEndPoints->pxNetworkInterface = NULL;
 
     pxNetworkEndPoints->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub;
     /* No assumption is added for pfOutput as its pointed to a static object/memory location. */

From e6e3b8174fb1e2d535d162846360739360e420e6 Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Wed, 15 Feb 2023 23:43:50 +0530
Subject: [PATCH 19/28] fixe minor isssue

---
 .../OutputARPRequest_harness.c                                  | 2 +-
 .../OutputARPRequest_harness.c                                  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

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 c5eab45c5b..8dbd0524a4 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
@@ -88,7 +88,7 @@ void harness()
 
     /* Interface init. */
     pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
-    pxNetworkEndPoints->pxNetworkInterface = NULL;
+    pxNetworkEndPoints->pxNetworkInterface->pxNext = NULL;
 
     pxNetworkEndPoints->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub;
     /* No assumption is added for pfOutput as its pointed to a static object/memory location. */
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 d7fcc2aa28..bf796e4e8a 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
@@ -71,7 +71,7 @@ void harness()
 
     /* Interface init. */
     pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
-    pxNetworkEndPoints->pxNetworkInterface = NULL;
+    pxNetworkEndPoints->pxNetworkInterface->pxNext = NULL;
 
     pxNetworkEndPoints->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub;
     /* No assumption is added for pfOutput as its pointed to a static object/memory location. */

From b1f9e463e25d2a2a93802af33fe91006f4211ea8 Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Thu, 16 Feb 2023 17:46:38 +0530
Subject: [PATCH 20/28] update asume to assignment

---
 test/FreeRTOS-Kernel                                            | 2 +-
 .../cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/test/FreeRTOS-Kernel b/test/FreeRTOS-Kernel
index 260a37c082..cb0757ee0b 160000
--- a/test/FreeRTOS-Kernel
+++ b/test/FreeRTOS-Kernel
@@ -1 +1 @@
-Subproject commit 260a37c082f4b70f9c6f361eadb0b29f1a448e3a
+Subproject commit cb0757ee0b8894090b82e75e83942e3c61a32245
diff --git a/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c b/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
index f95627c9a9..afd6e38ee8 100644
--- a/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
+++ b/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
@@ -69,7 +69,7 @@ void harness()
     */
     xNetworkBuffer2.pxEndPoint = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
     __CPROVER_assume( xNetworkBuffer2.pxEndPoint != NULL );
-    __CPROVER_assume( xNetworkBuffer2.pxEndPoint->pxNext == NULL );
+    xNetworkBuffer2.pxEndPoint->pxNext = NULL;
 
     eARPProcessPacket( &xNetworkBuffer2 );
 }

From f516277f06a3d2ad62f508fccc19816f3aad6082 Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Fri, 17 Feb 2023 11:16:20 +0530
Subject: [PATCH 21/28] more comments

---
 test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c          | 1 +
 .../cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c | 2 ++
 2 files changed, 3 insertions(+)

diff --git a/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c b/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c
index 39006e2f9c..b28f7ae362 100644
--- a/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c
+++ b/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c
@@ -29,6 +29,7 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes
 {
     __CPROVER_assert( pxDescriptor != NULL, "The network interface cannot be NULL." );
     __CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." );
+    __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "The Ethernet buffer cannot be NULL." );
     return 0;
 }
 
diff --git a/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c b/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
index afd6e38ee8..7aeac40d96 100644
--- a/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
+++ b/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
@@ -71,5 +71,7 @@ void harness()
     __CPROVER_assume( xNetworkBuffer2.pxEndPoint != NULL );
     xNetworkBuffer2.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 );
 }

From a338c5c53eb5f01db468f0914628905c7b5aa811 Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Fri, 17 Feb 2023 11:51:16 +0530
Subject: [PATCH 22/28] Revert "update asume to assignment"

This reverts commit b1f9e463e25d2a2a93802af33fe91006f4211ea8.
---
 test/FreeRTOS-Kernel                                            | 2 +-
 .../cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/test/FreeRTOS-Kernel b/test/FreeRTOS-Kernel
index cb0757ee0b..260a37c082 160000
--- a/test/FreeRTOS-Kernel
+++ b/test/FreeRTOS-Kernel
@@ -1 +1 @@
-Subproject commit cb0757ee0b8894090b82e75e83942e3c61a32245
+Subproject commit 260a37c082f4b70f9c6f361eadb0b29f1a448e3a
diff --git a/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c b/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
index 7aeac40d96..935af0e259 100644
--- a/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
+++ b/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
@@ -69,7 +69,7 @@ void harness()
     */
     xNetworkBuffer2.pxEndPoint = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
     __CPROVER_assume( xNetworkBuffer2.pxEndPoint != NULL );
-    xNetworkBuffer2.pxEndPoint->pxNext = NULL;
+    __CPROVER_assume( xNetworkBuffer2.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 );   */

From 49cbd5596b0d76a64c444c605fb27ec78b9a12d6 Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Fri, 17 Feb 2023 11:53:06 +0530
Subject: [PATCH 23/28] reverting kernel submodule change

---
 .../cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c b/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
index 935af0e259..7aeac40d96 100644
--- a/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
+++ b/test/cbmc/proofs/ARP/ARPProcessPacket/ARPProcessPacket_harness.c
@@ -69,7 +69,7 @@ void harness()
     */
     xNetworkBuffer2.pxEndPoint = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
     __CPROVER_assume( xNetworkBuffer2.pxEndPoint != NULL );
-    __CPROVER_assume( xNetworkBuffer2.pxEndPoint->pxNext == NULL );
+    xNetworkBuffer2.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 );   */

From 55a3ed93f3e6eaf7b8e0741e3f48880751e93ddb Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Fri, 17 Feb 2023 23:32:52 +0530
Subject: [PATCH 24/28] addding non deterministic number of endpoints

---
 .../ARPGetCacheEntry/ARPGetCacheEntry_harness.c | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

diff --git a/test/cbmc/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c b/test/cbmc/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c
index a845e9bb95..0b0456e3b2 100644
--- a/test/cbmc/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c
+++ b/test/cbmc/proofs/ARP/ARPGetCacheEntry/ARPGetCacheEntry_harness.c
@@ -21,15 +21,22 @@ void harness()
 
     pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
     __CPROVER_assume( pxNetworkEndPoints != NULL );
-    pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
-    __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
-    pxNetworkEndPoints->pxNext->pxNext = NULL;
 
     /* Interface init. */
     pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
     __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
-    pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
-    pxNetworkEndPoints->pxNext->pxNetworkInterface = NULL;
+
+    if( nondet_bool() )
+    {
+        pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+        __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
+        pxNetworkEndPoints->pxNext->pxNext = NULL;
+        pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
+    }
+    else
+    {
+        pxNetworkEndPoints->pxNext = NULL;
+    }
 
     NetworkInterface_t **ppxInterface = ( NetworkInterface_t ** ) malloc( sizeof( NetworkInterface_t * ) );
 

From 7e0a5b64d10bea4cc5e5ae981ba1ccbe76bc68ff Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Fri, 17 Feb 2023 23:42:05 +0530
Subject: [PATCH 25/28] addding non deterministic number of endpoints

---
 .../ARP/ARPAgeCache/ARPAgeCache_harness.c     | 19 +++++++++++++------
 .../ARPRefreshCacheEntry_harness.c            | 17 ++++++++++++-----
 2 files changed, 25 insertions(+), 11 deletions(-)

diff --git a/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c b/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c
index b28f7ae362..062e94d41a 100644
--- a/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c
+++ b/test/cbmc/proofs/ARP/ARPAgeCache/ARPAgeCache_harness.c
@@ -43,17 +43,24 @@ void harness()
 
     pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
     __CPROVER_assume( pxNetworkEndPoints != NULL );
-    pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
-    __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
-    pxNetworkEndPoints->pxNext->pxNext = NULL;
 
     /* Interface init. */
     pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
     __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
-    pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
-    pxNetworkEndPoints->pxNext->pxNetworkInterface = NULL;
 
-    pxNetworkEndPoints->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub;
+    if( nondet_bool() )
+    {
+        pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+        __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
+        pxNetworkEndPoints->pxNext->pxNext = NULL;
+        pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
+    }
+    else
+    {
+        pxNetworkEndPoints->pxNext = NULL;
+    }
+
+    pxNetworkEndPoints->pxNetworkInterface->pfOutput = NetworkInterfaceOutputFunction_Stub;
     /* No assumption is added for pfOutput as its pointed to a static object/memory location. */
     
     vARPAgeCache();
diff --git a/test/cbmc/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c b/test/cbmc/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c
index 9b654e5fa9..c0c550501f 100644
--- a/test/cbmc/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c
+++ b/test/cbmc/proofs/ARP/ARPRefreshCacheEntry/ARPRefreshCacheEntry_harness.c
@@ -19,15 +19,22 @@ void harness()
 
     pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
     __CPROVER_assume( pxNetworkEndPoints != NULL );
-    pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
-    __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
-    pxNetworkEndPoints->pxNext->pxNext = NULL;
 
     /* Interface init. */
     pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
     __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
-    pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
-    pxNetworkEndPoints->pxNext->pxNetworkInterface = NULL;
+
+    if( nondet_bool() )
+    {
+        pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+        __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
+        pxNetworkEndPoints->pxNext->pxNext = NULL;
+        pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
+    }
+    else
+    {
+        pxNetworkEndPoints->pxNext = NULL;
+    }
 
 
     NetworkEndPoint_t * pxEndPoint = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );

From 195e024a1a9961a04274c537ae8b84bbfa33fef8 Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Fri, 17 Feb 2023 23:45:45 +0530
Subject: [PATCH 26/28] addding non deterministic number of endpoints

---
 .../OutputARPRequest_harness.c                  | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

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 36a9487d09..f5a5842289 100644
--- a/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c
+++ b/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c
@@ -95,15 +95,22 @@ void harness()
 
     pxNetworkEndPoints = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
     __CPROVER_assume( pxNetworkEndPoints != NULL );
-    pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
-    __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
-    pxNetworkEndPoints->pxNext->pxNext = NULL;
 
     /* Interface init. */
     pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
     __CPROVER_assume( pxNetworkEndPoints->pxNetworkInterface != NULL );
-    pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
-    pxNetworkEndPoints->pxNext->pxNetworkInterface = NULL;
+
+    if( nondet_bool() )
+    {
+        pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) malloc( sizeof( NetworkEndPoint_t ) );
+        __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
+        pxNetworkEndPoints->pxNext->pxNext = NULL;
+        pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkEndPoints->pxNetworkInterface;
+    }
+    else
+    {
+        pxNetworkEndPoints->pxNext = NULL;
+    }
 
     pxNetworkEndPoints->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub;
     /* No assumption is added for pfOutput as its pointed to a static object/memory location. */

From e9c886150cc659e0d096c6a23f116f37b383a215 Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Fri, 17 Feb 2023 23:53:30 +0530
Subject: [PATCH 27/28] addding non deterministic number of endpoints

---
 .../OutputARPRequest_harness.c                               | 5 ++++-
 .../OutputARPRequest_harness.c                               | 3 ++-
 2 files changed, 6 insertions(+), 2 deletions(-)

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 8dbd0524a4..292910625d 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
@@ -65,6 +65,9 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes
                                                 NetworkBufferDescriptor_t * const pxNetworkBuffer,
                                                 BaseType_t xReleaseAfterSend )
 {
+    __CPROVER_assert( pxDescriptor != NULL, "The network interface cannot be NULL." );
+    __CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." );
+    __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "The ethernet buffer cannot be NULL." );
     if( xReleaseAfterSend != pdFALSE )
     {
         vReleaseNetworkBufferAndDescriptor( pxNetworkBuffer );
@@ -90,7 +93,7 @@ void harness()
     pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
     pxNetworkEndPoints->pxNetworkInterface->pxNext = NULL;
 
-    pxNetworkEndPoints->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub;
+    pxNetworkEndPoints->pxNetworkInterface->pfOutput = NetworkInterfaceOutputFunction_Stub;
     /* No assumption is added for pfOutput as its pointed to a static object/memory location. */
 
     if( xRes == pdPASS )
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 bf796e4e8a..779e92f9c9 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
@@ -48,6 +48,7 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes
 
     __CPROVER_assert( pxDescriptor != NULL, "The network interface cannot be NULL." );
     __CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." );
+    __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "The ethernet buffer cannot be NULL." );
     
     if( xReleaseAfterSend != pdFALSE )
     {
@@ -73,7 +74,7 @@ void harness()
     pxNetworkEndPoints->pxNetworkInterface = ( NetworkInterface_t * ) malloc( sizeof( NetworkInterface_t ) );
     pxNetworkEndPoints->pxNetworkInterface->pxNext = NULL;
 
-    pxNetworkEndPoints->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub;
+    pxNetworkEndPoints->pxNetworkInterface->pfOutput = NetworkInterfaceOutputFunction_Stub;
     /* No assumption is added for pfOutput as its pointed to a static object/memory location. */
 
     if( xRes == pdPASS )

From 4954db6a3ae3078b207e23242a16da60a64ffd51 Mon Sep 17 00:00:00 2001
From: tony-josi-aws <tonyjosi@amazon.com>
Date: Fri, 17 Feb 2023 23:54:43 +0530
Subject: [PATCH 28/28] addding non deterministic number of endpoints

---
 .../ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c | 1 +
 1 file changed, 1 insertion(+)

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 f5a5842289..c3b1ab390d 100644
--- a/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c
+++ b/test/cbmc/proofs/ARP/ARP_FreeRTOS_OutputARPRequest/OutputARPRequest_harness.c
@@ -79,6 +79,7 @@ BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDes
 
     __CPROVER_assert( pxDescriptor != NULL, "The network interface cannot be NULL." );
     __CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." );
+    __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "The ethernet buffer cannot be NULL." );
 
 }