30     FreeRTOS_Socket_t * pxSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) );  in harness()  local
33     __CPROVER_assume( pxSocket != NULL );  in harness()
34     __CPROVER_assume( pxSocket != FREERTOS_INVALID_SOCKET );  in harness()
40     pxSocket->pxUserWakeCallback = safeMalloc( sizeof( SocketWakeupCallback_t ) );  in harness()
45         pxSocket->xEventGroup = xEventGroupCreate();  in harness()
46         __CPROVER_assume( pxSocket->xEventGroup != NULL );  in harness()
50         pxSocket->xEventGroup = NULL;  in harness()
61         vListInitialiseItem( &( pxSocket->xBoundSocketListItem ) );  in harness()
62         pxSocket->xBoundSocketListItem.pxContainer = &( BoundSocketList );  in harness()
63         vListInsertEnd( &BoundSocketList, &( pxSocket->xBoundSocketListItem ) );  in harness()
67         pxSocket->xBoundSocketListItem.pxContainer = NULL;  in harness()
71     pxSocket->ucProtocol = PROTOCOL;  in harness()
77     if( pxSocket->ucProtocol == FREERTOS_IPPROTO_TCP )  in harness()
79         pxSocket->u.xTCP.rxStream = malloc( sizeof( StreamBuffer_t ) );  in harness()
80         pxSocket->u.xTCP.txStream = malloc( sizeof( StreamBuffer_t ) );  in harness()
85 …pxSocket->u.xTCP.pxAckMessage = pxGetNetworkBufferWithDescriptor( xRequestedSizeBytes, xBlockTimeT…  in harness()
89             pxSocket->u.xTCP.pxAckMessage = NULL;  in harness()
92     else if( pxSocket->ucProtocol == FREERTOS_IPPROTO_UDP )  in harness()
95         vListInitialise( &( pxSocket->u.xUDP.xWaitingPacketsList ) );  in harness()
111             NetworkBuffer->xBufferListItem.pxContainer = &( pxSocket->u.xUDP.xWaitingPacketsList );  in harness()
114 …  vListInsertEnd( &( pxSocket->u.xUDP.xWaitingPacketsList ), &( NetworkBuffer->xBufferListItem ) );  in harness()
122     vSocketClose( pxSocket );  in harness()