FreeRTOS/FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/test/cbmc/proofs/ARP/ARPGenerateRequestPacket
Given that the pointer target of xNetworkDescriptor.pucEthernetBuffer is allocated to the size claimed in xNetworkDescriptor.xDataLength, this harness proves the memory safety of ARPGenerateRequestPacket.