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 
10 /* This pointer is maintained by the IP-task. Defined in FreeRTOS_IP.c */
11 extern NetworkBufferDescriptor_t * pxARPWaitingNetworkBuffer;
12 
13 /* This is an output function and need not be tested with this proof. */
FreeRTOS_OutputARPRequest(uint32_t ulIPAddress)14 void FreeRTOS_OutputARPRequest( uint32_t ulIPAddress )
15 {
16 }
17 
harness()18 void harness()
19 {
20     ARPPacket_t xARPFrame;
21     NetworkBufferDescriptor_t xLocalBuffer;
22     uint16_t usEthernetBufferSize;
23 
24     /* Non deterministically determine whether the pxARPWaitingNetworkBuffer will
25      * point to some valid data or will it be NULL. */
26     if( nondet_bool() )
27     {
28         /* The packet must at least be as big as an IP Packet. The size is not
29          * checked in the function as the pointer is stored by the IP-task itself
30          * and therefore it will always be of the required size. */
31         __CPROVER_assume( usEthernetBufferSize >= sizeof( IPPacket_t ) );
32 
33         /* Add matching data length to the network buffer descriptor. */
34         __CPROVER_assume( xLocalBuffer.xDataLength == usEthernetBufferSize );
35 
36         xLocalBuffer.pucEthernetBuffer = malloc( usEthernetBufferSize );
37 
38         /* Since this pointer is maintained by the IP-task, either the pointer
39          * pxARPWaitingNetworkBuffer will be NULL or xLocalBuffer.pucEthernetBuffer
40          * will be non-NULL. */
41         __CPROVER_assume( xLocalBuffer.pucEthernetBuffer != NULL );
42 
43         pxARPWaitingNetworkBuffer = &xLocalBuffer;
44     }
45     else
46     {
47         pxARPWaitingNetworkBuffer = NULL;
48     }
49 
50     eARPProcessPacket( &xARPFrame );
51 }
52