29                         FreeRTOS_Socket_t * const pxSocket );
49     FreeRTOS_Socket_t * pxSocket = malloc( sizeof( FreeRTOS_Socket_t ) );  in harness()  local
51     __CPROVER_assume( pxSocket != NULL );  in harness()
53     pxSocket->u.xTCP.txStream = malloc( sizeof( StreamBuffer_t ) );  in harness()
54     __CPROVER_assume( pxSocket->u.xTCP.txStream != NULL );  in harness()
56     vListInitialise( &pxSocket->u.xTCP.xTCPWindow.xWaitQueue );  in harness()
63         vListInsertEnd( &pxSocket->u.xTCP.xTCPWindow.xWaitQueue, &segment->xQueueItem );  in harness()
66     vListInitialise( &pxSocket->u.xTCP.xTCPWindow.xTxSegments );  in harness()
74         vListInsertEnd( &pxSocket->u.xTCP.xTCPWindow.xTxSegments, &segment->xQueueItem );  in harness()
77     vListInitialise( &pxSocket->u.xTCP.xTCPWindow.xPriorityQueue );  in harness()
99     __CPROVER_assume( pxSocket != NULL );  in harness()
101     prvReadSackOption( pucPtr, uxIndex, pxSocket );  in harness()