Searched refs:uxItemSize (Results 1 – 2 of 2) sorted by relevance
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() local79 __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() local123 __CPROVER_assume( uxItemSize < uxQueueStorageSize / uxQueueLength ); in xUnconstrainedQueue()[all …]
72 UBaseType_t uxItemSize; member108 … __CPROVER_assert( !( ( pvItemToQueue == NULL ) && ( xQueue->uxItemSize != ( UBaseType_t ) 0U ) ), in xQueueGenericSend()158 __CPROVER_assume( pxSocket->pxUserSemaphore->uxItemSize == 0 ); in harness()
