path: root/FreeRTOS-Plus/Test/CBMC/proofs/ARP/ARPGenerateRequestPacket/README.md

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.