Home
last modified time | relevance | path

Searched refs:uxMessagesWaiting (Results 1 – 2 of 2) sorted by relevance

/FreeRTOS-Plus-TCP-v3.1.0/test/cbmc/include/
HDqueue_init.h57 xSet->uxMessagesWaiting = nondet_UBaseType_t(); in xUnconstrainedQueueSet()
62 __CPROVER_assume( xSet->uxMessagesWaiting < xSet->uxLength ); in xUnconstrainedQueueSet()
95 xQueue->uxMessagesWaiting = nondet_UBaseType_t(); in xUnconstrainedQueueBoundedItemSize()
99 __CPROVER_assume( xQueue->uxMessagesWaiting < xQueue->uxLength ); in xUnconstrainedQueueBoundedItemSize()
133 xQueue->uxMessagesWaiting = nondet_UBaseType_t(); in xUnconstrainedQueue()
137 __CPROVER_assume( xQueue->uxMessagesWaiting < xQueue->uxLength ); in xUnconstrainedQueue()
160 xQueue->uxMessagesWaiting = nondet_UBaseType_t(); in xUnconstrainedMutex()
164 __CPROVER_assume( xQueue->uxMessagesWaiting < xQueue->uxLength ); in xUnconstrainedMutex()
/FreeRTOS-Plus-TCP-v3.1.0/test/cbmc/proofs/Socket/vSocketWakeUpUser/
HDvSocketWakeUpUser_harness.c70 volatile UBaseType_t uxMessagesWaiting; member