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 #include "FreeRTOS_UDP_IP.h"
10 #include "FreeRTOS_TCP_IP.h"
11 
12 /*This proof assumes that pxUDPSocketLookup is implemented correctly. */
13 
14 /* This proof was done before. Hence we assume it to be correct here. */
vARPRefreshCacheEntry(const MACAddress_t * pxMACAddress,const uint32_t ulIPAddress)15 void vARPRefreshCacheEntry( const MACAddress_t * pxMACAddress,
16                             const uint32_t ulIPAddress )
17 {
18 }
19 
20 /* This proof was done before. Hence we assume it to be correct here. */
xIsDHCPSocket(Socket_t xSocket)21 BaseType_t xIsDHCPSocket( Socket_t xSocket )
22 {
23 }
24 
25 /* This proof was done before. Hence we assume it to be correct here. */
ulDNSHandlePacket(NetworkBufferDescriptor_t * pxNetworkBuffer)26 uint32_t ulDNSHandlePacket( NetworkBufferDescriptor_t * pxNetworkBuffer )
27 {
28 }
29 
30 /* Implementation of safe malloc */
safeMalloc(size_t xWantedSize)31 void * safeMalloc( size_t xWantedSize )
32 {
33     if( xWantedSize == 0 )
34     {
35         return NULL;
36     }
37 
38     uint8_t byte;
39 
40     return byte ? malloc( xWantedSize ) : NULL;
41 }
42 
43 /* Abstraction of pxUDPSocketLookup */
pxUDPSocketLookup(UBaseType_t uxLocalPort)44 FreeRTOS_Socket_t * pxUDPSocketLookup( UBaseType_t uxLocalPort )
45 {
46     return safeMalloc( sizeof( FreeRTOS_Socket_t ) );
47 }
48 
harness()49 void harness()
50 {
51     NetworkBufferDescriptor_t * pxNetworkBuffer = safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
52     BaseType_t * pxIsWaitingForARPResolution;
53 
54     pxIsWaitingForARPResolution = safeMalloc( sizeof( BaseType_t ) );
55 
56     /* The function under test is only called by the IP-task. The below pointer is an
57      * address of a local variable which is being passed to the function under test.
58      * Thus, it cannot ever be NULL. */
59     __CPROVER_assume( pxIsWaitingForARPResolution != NULL );
60 
61     if( pxNetworkBuffer )
62     {
63         pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( UDPPacket_t ) );
64     }
65 
66     uint16_t usPort;
67 
68     if( pxNetworkBuffer && pxNetworkBuffer->pucEthernetBuffer )
69     {
70         xProcessReceivedUDPPacket( pxNetworkBuffer, usPort, pxIsWaitingForARPResolution );
71     }
72 }
73