more comments

Author: tony-josi-aws

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;
 }
 

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 );
 }