136     FreeRTOS_Socket_t * pxSocket = ensure_FreeRTOS_Socket_t_is_allocated();  in harness()  local
138     __CPROVER_assume( pxSocket != NULL );  in harness()
139     __CPROVER_assume( pxSocket != FREERTOS_INVALID_SOCKET );  in harness()
141     pxSocket->pxUserWakeCallback = safeMalloc( sizeof( SocketWakeupCallback_t ) );  in harness()
143     pxSocket->pxSocketSet = safeMalloc( sizeof( struct xSOCKET_SET ) );  in harness()
145     if( pxSocket->pxSocketSet != NULL )  in harness()
147         pxSocket->pxSocketSet->xSelectGroup = safeMalloc( sizeof( struct EventGroupDef_t ) );  in harness()
150         __CPROVER_assume( pxSocket->pxSocketSet->xSelectGroup != NULL );  in harness()
153     pxSocket->pxUserSemaphore = safeMalloc( sizeof( xQUEUE ) );  in harness()
155     if( pxSocket->pxUserSemaphore != NULL )  in harness()
158         __CPROVER_assume( pxSocket->pxUserSemaphore->uxItemSize == 0 );  in harness()
161     pxSocket->xEventGroup = safeMalloc( sizeof( struct EventGroupDef_t ) );  in harness()
166     vSocketWakeUpUser( pxSocket );  in harness()