1 /* FreeRTOS includes. */
2 #include "FreeRTOS.h"
3 #include "queue.h"
4 
5 /* FreeRTOS+TCP includes. */
6 #include "FreeRTOS_IP.h"
7 #include "FreeRTOS_IP_Private.h"
8 #include "FreeRTOS_ARP.h"
9 
harness()10 void harness()
11 {
12     /*
13      * The assumption made here is that the buffer pointed by pucEthernetBuffer
14      * is at least allocated to sizeof(ARPPacket_t) size but eventually a even larger buffer.
15      * This is not checked inside vARPGenerateRequestPacket.
16      */
17     uint8_t ucBUFFER_SIZE;
18 
19     __CPROVER_assume( ucBUFFER_SIZE >= sizeof( ARPPacket_t ) && ucBUFFER_SIZE < 2 * sizeof( ARPPacket_t ) );
20     void * xBuffer = malloc( ucBUFFER_SIZE );
21 
22     __CPROVER_assume( xBuffer != NULL );
23 
24     NetworkBufferDescriptor_t xNetworkBuffer2;
25 
26     xNetworkBuffer2.pucEthernetBuffer = xBuffer;
27     xNetworkBuffer2.xDataLength = ucBUFFER_SIZE;
28 
29     /* vARPGenerateRequestPacket asserts buffer has room for a packet */
30     __CPROVER_assume( xNetworkBuffer2.xDataLength >= sizeof( ARPPacket_t ) );
31     vARPGenerateRequestPacket( &xNetworkBuffer2 );
32 }
33