33 …__CPROVER_assert( __CPROVER_w_ok( ( void * ) pxQueue->u.xQueue.pcReadFrom, ( size_t ) pxQueue->uxI…  in prvCopyDataToQueue()
87     QueueHandle_t xQueue =  in xUnconstrainedQueueBoundedItemSize()  local
90     if( xQueue )  in xUnconstrainedQueueBoundedItemSize()
92         xQueue->cTxLock = nondet_int8_t();  in xUnconstrainedQueueBoundedItemSize()
93         __CPROVER_assume( xQueue->cTxLock != 127 );  in xUnconstrainedQueueBoundedItemSize()
94         xQueue->cRxLock = nondet_int8_t();  in xUnconstrainedQueueBoundedItemSize()
95         xQueue->uxMessagesWaiting = nondet_UBaseType_t();  in xUnconstrainedQueueBoundedItemSize()
99         __CPROVER_assume( xQueue->uxMessagesWaiting < xQueue->uxLength );  in xUnconstrainedQueueBoundedItemSize()
100         xQueue->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t();  in xUnconstrainedQueueBoundedItemSize()
101         xQueue->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t();  in xUnconstrainedQueueBoundedItemSize()
103             xQueueAddToSet( xQueue, xUnconstrainedQueueSet() );  in xUnconstrainedQueueBoundedItemSize()
107     return xQueue;  in xUnconstrainedQueueBoundedItemSize()
125     QueueHandle_t xQueue =  in xUnconstrainedQueue()  local
128     if( xQueue )  in xUnconstrainedQueue()
130         xQueue->cTxLock = nondet_int8_t();  in xUnconstrainedQueue()
131         __CPROVER_assume( xQueue->cTxLock != 127 );  in xUnconstrainedQueue()
132         xQueue->cRxLock = nondet_int8_t();  in xUnconstrainedQueue()
133         xQueue->uxMessagesWaiting = nondet_UBaseType_t();  in xUnconstrainedQueue()
137         __CPROVER_assume( xQueue->uxMessagesWaiting < xQueue->uxLength );  in xUnconstrainedQueue()
138         xQueue->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t();  in xUnconstrainedQueue()
139         xQueue->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t();  in xUnconstrainedQueue()
141             xQueueAddToSet( xQueue, xUnconstrainedQueueSet() );  in xUnconstrainedQueue()
145     return xQueue;  in xUnconstrainedQueue()
152     QueueHandle_t xQueue =  in xUnconstrainedMutex()  local
155     if( xQueue )  in xUnconstrainedMutex()
157         xQueue->cTxLock = nondet_int8_t();  in xUnconstrainedMutex()
158         __CPROVER_assume( xQueue->cTxLock != 127 );  in xUnconstrainedMutex()
159         xQueue->cRxLock = nondet_int8_t();  in xUnconstrainedMutex()
160         xQueue->uxMessagesWaiting = nondet_UBaseType_t();  in xUnconstrainedMutex()
164         __CPROVER_assume( xQueue->uxMessagesWaiting < xQueue->uxLength );  in xUnconstrainedMutex()
165         xQueue->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t();  in xUnconstrainedMutex()
166         xQueue->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t();  in xUnconstrainedMutex()
168             xQueueAddToSet( xQueue, xUnconstrainedQueueSet() );  in xUnconstrainedMutex()
172     return xQueue;  in xUnconstrainedMutex()