Fix CBMC proofs

Author: tony-josi-aws

test/cbmc/proofs/ARP/ARPGetCacheEntry/Configurations.json

@@ -6,6 +6,7 @@
       "--unwindset prvCacheLookup.0:7",
       "--unwindset FreeRTOS_FindEndPointOnIP_IPv4.0:3",
       "--unwindset FreeRTOS_InterfaceEndPointOnNetMask.0:3",
+      "--unwindset xIsIPv4Broadcast.0:3",
       "--unwindset eARPGetCacheEntry.0:3",
       "--unwindset FreeRTOS_FindGateWay.0:3",
       "--nondet-static"

test/cbmc/proofs/parsing/ProcessIPPacket/ProcessIPPacket_harness.c

@@ -157,7 +157,8 @@ 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;
-
+    NetworkEndPoint_t xEndPoint;
+    
     __CPROVER_assume( pxNetworkBuffer != NULL );
     __CPROVER_assume( pucEthernetBuffer != NULL );
 
@@ -166,6 +167,19 @@ void harness()
     pxNetworkBuffer->pucEthernetBuffer = &( pucEthernetBuffer[ ipIP_TYPE_OFFSET ] );
     __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
 
+    /* prvProcessIPPacket is guranteed to receive a network buffer that has a valid
+    endpoint, hence no NULL checks are needed to be performed inside prvProcessIPPacket.
+    See the check:
+        
+        if( ( pxNetworkBuffer->pxInterface == NULL ) || ( pxNetworkBuffer->pxEndPoint == NULL ) )
+        {
+            break;
+        }
+
+    inside the prvProcessEthernetPacket before which prvProcessIPPacket is called.
+     */
+    pxNetworkBuffer->pxEndPoint = &xEndPoint;
+
     /* Minimum length of the pxNetworkBuffer->xDataLength is at least the size of the IPPacket_t. */
     __CPROVER_assume( pxNetworkBuffer->xDataLength >= sizeof( IPPacket_t ) && pxNetworkBuffer->xDataLength <= ipTOTAL_ETHERNET_FRAME_SIZE );