23         if( pxQueue->uxItemSize > ( UBaseType_t ) 0 )  in prvCopyDataToQueue()
25 …__CPROVER_assert( __CPROVER_r_ok( pvItemToQueue, ( size_t ) pxQueue->uxItemSize ), "pvItemToQueue …  in prvCopyDataToQueue()
29 …rt( __CPROVER_w_ok( ( void * ) pxQueue->pcWriteTo, ( size_t ) pxQueue->uxItemSize ), "pxQueue->pcW…  in prvCopyDataToQueue()
33 …VER_w_ok( ( void * ) pxQueue->u.xQueue.pcReadFrom, ( size_t ) pxQueue->uxItemSize ), "pxQueue->u.x…  in prvCopyDataToQueue()
75     UBaseType_t uxItemSize;  in xUnconstrainedQueueBoundedItemSize()  local
79     __CPROVER_assume( uxItemSize < uxItemSizeBound );  in xUnconstrainedQueueBoundedItemSize()
85     __CPROVER_assume( uxItemSize < uxQueueStorageSize / uxQueueLength );  in xUnconstrainedQueueBoundedItemSize()
88         xQueueGenericCreate( uxQueueLength, uxItemSize, ucQueueType );  in xUnconstrainedQueueBoundedItemSize()
114     UBaseType_t uxItemSize;  in xUnconstrainedQueue()  local
123     __CPROVER_assume( uxItemSize < uxQueueStorageSize / uxQueueLength );  in xUnconstrainedQueue()
126         xQueueGenericCreate( uxQueueLength, uxItemSize, ucQueueType );  in xUnconstrainedQueue()