Fix CBMC proof for xCheckRequiresARPResolution

Author: tony-josi-aws

test/cbmc/proofs/ARP/xCheckRequiresARPResolution/xCheckRequiresARPResolution_harness.c

@@ -90,18 +90,12 @@ void harness()
     NetworkBufferDescriptor_t * pxNetworkBuffer;
     IPPacket_t * pxIPPacket;
 
-    /* IPv4/IPv6 header size are different. To make sure buffer size is enough,
-     * determine the test case is for IPv4 or IPv6 at the beginning. */
-    xIsIPv6 = nondet_bool();
+    const IPPacket_t * pxIPPacket;
+    const IPHeader_t * pxIPHeader;
 
-    if( xIsIPv6 )
-    {
-        __CPROVER_assume( ( xBufferLength >= sizeof( IPPacket_IPv6_t ) ) && ( xBufferLength < ipconfigNETWORK_MTU ) );
-    }
-    else
-    {
-        __CPROVER_assume( ( xBufferLength >= sizeof( IPPacket_t ) ) && ( xBufferLength < ipconfigNETWORK_MTU ) );
-    }
+    /* Make sure buffer size is enough, xCheckRequiresARPResolution is only called for
+    IPv4 packets hence the minimum size should be  sizeof( IPPacket_t ) */
+    __CPROVER_assume( ( xBufferLength >= sizeof( IPPacket_t ) ) && ( xBufferLength < ipconfigNETWORK_MTU ) );
 
     pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
     __CPROVER_assume( pxNetworkBuffer != NULL );
@@ -111,6 +105,13 @@ void harness()
     pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xBufferLength );
     __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
 
+    /* Its asserted in the code that xCheckRequiresARPResolution is only called on IPv4 frame types */
+    /* See assertion: configASSERT( ( pxIPPacket->xEthernetHeader.usFrameType == ipIPv4_FRAME_TYPE ) || ( pxIPPacket->xEthernetHeader.usFrameType == ipARP_FRAME_TYPE ) );
+    in xCheckRequiresARPResolution() */
+    pxIPPacket = ( ( const IPPacket_t * ) pxNetworkBuffer->pucEthernetBuffer );
+    pxIPHeader = &( pxIPPacket->xIPHeader );
+    __CPROVER_assume(pxIPPacket->xEthernetHeader.usFrameType == ipIPv4_FRAME_TYPE);
+
     pxNetworkBuffer->pxEndPoint = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
     __CPROVER_assume( pxNetworkBuffer->pxEndPoint != NULL );